tendsto_coe_sub — Mathlib

English

The map n ↦ (n)⁻¹ converges to 0 as n tends to atTop in the natural numbers, viewed in ENNReal.

Русский

Функция n ↦ n⁻¹ сходится к 0 при n→∞ (в счётном множестве), если рассматривать ENNReal.

LaTeX

$$$\\text{Tendsto}(n \\mapsto (n : ENNReal)^{-1})\\text{ atTop }(\\mathcal{N} 0).$$$

Lean4

protected theorem tendsto_coe_sub {b : ℝ≥0∞} : Tendsto (fun b : ℝ≥0∞ => ↑r - b) (𝓝 b) (𝓝 (↑r - b)) :=
  continuous_nnreal_sub.tendsto _

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