tendsto_pow_atTop — Mathlib

English

For any natural n with n ≠ 0, the map x ↦ x^n tends to +∞ as x → +∞.

Русский

Для любого натурального n, отличного от нуля, отображение x ↦ x^n стремится к +∞ при x → +∞.

LaTeX

$$$ \forall n \in \mathbb{N}, n \neq 0 \Rightarrow \lim_{x \to +\infty} x^n = +\infty. $$$

Lean4

/-- The monomial function `x^n` tends to `+∞` at `+∞` for any positive natural `n`.
A version for positive real powers exists as `tendsto_rpow_atTop`. -/
theorem tendsto_pow_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (fun x : α => x ^ n) atTop atTop :=
  tendsto_atTop_mono' _ ((eventually_ge_atTop 1).mono fun _x hx => le_self_pow₀ hx hn) tendsto_id

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