tendsto_pow_atTop_nhds_zero_iff — Mathlib

English

For NNReal numbers r, the sequence r^n tends to 0 as n → ∞ if and only if r < 1.

Русский

Для числа NNReal выполняется: r^n → 0 ⇔ r < 1.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{N\\\\!NReal}, \\\\ operatorname{Tendsto}(n \\\\mapsto r^n) \\\\ atTop \\\\ (\\\\mathcal{N} 0) \\\\Leftrightarrow \\\\ r < 1.$$$

Lean4

@[simp]
protected theorem tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 :=
  ⟨fun h => by
    simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
      tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h,
    tendsto_pow_atTop_nhds_zero_of_lt_one⟩

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