abs_tendsto_atTop_iff — Mathlib

English

As x → ∞, |P(x)| → ∞ if and only if deg P > 0.

Русский

При x, стремящемся к бесконечности, модуль многочлена растет без границы тогда и только тогда, когда deg P > 0.

LaTeX

$$$$\operatorname{Tendsto}\bigl(x \mapsto |P(x)|\bigr)\;\text{atTop}\;\text{atTop} \iff 0 < \deg P.$$$$

Lean4

theorem abs_tendsto_atTop_iff : Tendsto (fun x => abs <| eval x P) atTop atTop ↔ 0 < P.degree :=
  ⟨fun h => not_le.mp (mt (abs_isBoundedUnder_iff P).mpr (not_isBoundedUnder_of_tendsto_atTop h)), abs_tendsto_atTop P⟩

Похожие утверждения