𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => abs (eval x P)
⊢ degree P ≤ 0
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => abs (eval x P)) ↔ degree P ≤ 0
refine' ⟨fun h => _, fun h => ⟨|P.coeff 0|, eventually_map.mpr (eventually_of_forall
  (forall_imp (fun _ => le_of_eq) fun x => congr_arg abs <| _root_.trans (congr_arg (eval x)
  (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : 0 < degree P
⊢ ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => abs (eval x P)
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => abs (eval x P)
⊢ degree P ≤ 0
contrapose! h
no goals
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : 0 < degree P
⊢ ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => abs (eval x P)
exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)