tendsto_pow_neg_atTop — Mathlib

English

For any n > 0, the function x^{-n} tends to 0 as x tends to +∞.

Русский

Для любого натурального n > 0 функция x^{-n} стремится к 0 при x → +∞.

LaTeX

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

Lean4

/-- The function `x^(-n)` tends to `0` at `+∞` for any positive natural `n`.
A version for positive real powers exists as `tendsto_rpow_neg_atTop`. -/
theorem tendsto_pow_neg_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0) := by
  simpa only [zpow_neg, zpow_natCast] using (tendsto_pow_atTop (α := 𝕜) hn).inv_tendsto_atTop

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