English
Tendsto f to top in ENat is equivalent to: for all n ∈ ℕ, eventually n < f(a).
Русский
Сходится к верхнему пределу в ENat тогда и только тогда, когда для каждого n ∈ ℕ тождественно выполняется n < f(a) eventually.
LaTeX
$$$$\\forall \\alpha, \\; \\operatorname{Tendsto}(f,l,\\mathcal{N}_{\\top}) \\iff \\forall n \\in \\mathbb{N}, \\; \\text{eventually } (n < f(a)).$$$$
Lean4
theorem tendsto_nhds_top_iff_natCast_lt {α : Type*} {l : Filter α} {f : α → ℕ∞} :
Tendsto f l (𝓝 ⊤) ↔ ∀ n : ℕ, ∀ᶠ a in l, n < f a := by
simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top, mem_Ioi]