English
Let m : α → ENNReal and f : Filter α. The limit to ∞ is equivalent to: for every natural number n, m a eventually exceeds the real number n.
Русский
Пусть m : α → ENNReal и f : Filter α. Предел к бесконечности эквивалентен тому, что для каждого натурального числа n множество a с m a > n принадлежит f вплоть до скользящих моментов.
LaTeX
$$$\\operatorname{Tendsto} m f (\\mathcal{N}(\\infty)) \\iff \\forall n \\in \\mathbb{N}, \\forall^{\\infty} a \\in f, \\uparrow n < m a$$$
Lean4
theorem tendsto_nhds_top_iff_nat {m : α → ℝ≥0∞} {f : Filter α} : Tendsto m f (𝓝 ∞) ↔ ∀ n : ℕ, ∀ᶠ a in f, ↑n < m a :=
tendsto_nhds_top_iff_nnreal.trans
⟨fun h n => by simpa only [ENNReal.coe_natCast] using h n, fun h x =>
let ⟨n, hn⟩ := exists_nat_gt x
(h n).mono fun _ => lt_trans <| by rwa [← ENNReal.coe_natCast, coe_lt_coe]⟩
