tendsto_pow_atTop_iff — Mathlib

English

Let α be a linearly ordered ring with a semiring structure. For every natural number n, the function x ↦ x^n tends to infinity as x tends to infinity if and only if n ≠ 0.

Русский

Пусть α — упорядоченное кольцо с полупрямой структурой, тогда для каждого натурального n функция x ↦ x^n стремится к бесконечности при x → ∞ тогда и только тогда, когда n ≠ 0.

LaTeX

$$$$\lim_{x \to \infty} x^n = \infty \quad \text{iff} \quad n \neq 0.$$$$

Lean4

@[simp]
theorem tendsto_pow_atTop_iff {n : ℕ} : Tendsto (fun x : α => x ^ n) atTop atTop ↔ n ≠ 0 :=
  ⟨fun h hn => by simp only [hn, pow_zero, not_tendsto_const_atTop] at h, tendsto_pow_atTop⟩

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