tendsto_nat_nhds_top — Mathlib

English

The natural numbers converge to infinity in ENNReal via the cast map; i.e., the sequence n ↦ n.cast tends to infinity along atTop.

Русский

Натуральные числа сходятся к бесконечности в ENNReal через отображение приведения; то есть последовательность n \\mapsto n.cast сходится к бесконечности вдоль atTop.

LaTeX

$$$\\operatorname{Tendsto}(n \\mapsto n.\\cast) \\text{Filter.atTop} \\left(\\mathcal{N}(\\infty)\\right)$$$

Lean4

theorem tendsto_nat_nhds_top : Tendsto (fun n : ℕ => ↑n) atTop (𝓝 ∞) :=
  tendsto_nhds_top fun n => mem_atTop_sets.2 ⟨n + 1, fun _m hm => mem_setOf.2 <| Nat.cast_lt.2 <| Nat.lt_of_succ_le hm⟩

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