Theorems · Theorem · real analysis

Polynomial.isBoundedUnder_abs_atBot_iff

∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atBot fun x => |Polynomial.eval x P|) ↔ P.degree ≤ 0

Defined in

Mathlib.Analysis.Polynomial.Basic

Cited by

1 results in Mathlib

Foundations

Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldLinearOrderIsStrictOrderedRingOrderTopology