tendsto_pow_atTop_nhds_zero_of_lt_one

English

If r is a nonnegative extended real with r < 1, then r^n → 0 as n → ∞.

Русский

Если r ∈ ℝ≥0∞ и r < 1, то r^n → 0 при n → ∞.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{R}_{\\\\ge 0}\\\\infty, \\\\ r < 1 \\\\Rightarrow \\\\ operatorname{Tendsto}(n \\\\mapsto r^n) \\\\ atTop \\\\ (\\\\mathcal{N} 0).$$$

Lean4

theorem tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < 1) : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) :=
  by
  rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
  rw [← ENNReal.coe_zero]
  norm_cast at *
  apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr

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