abs_tendsto_atTop — Mathlib

English

Let 𝕜 be a normed ordered field. If P ∈ 𝕜[X] has positive degree, then |P(x)| tends to infinity as x tends to infinity.

Русский

Пусть 𝕜 — нормированное упорядоченное поле. Если P ∈ 𝕜[X] имеет положительную степень, то |P(x)| стремится к бесконечности при x → ∞.

LaTeX

$$$$ \deg P > 0 \implies \lim_{x \to \infty} |P(x)| = \infty.$$$$

Lean4

theorem abs_tendsto_atTop (hdeg : 0 < P.degree) : Tendsto (fun x => abs <| eval x P) atTop atTop :=
  by
  rcases le_total 0 P.leadingCoeff with hP | hP
  · exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)
  · exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)

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