English
Equivalently characterize convergence to the top in ENat by a uniform lower bound by natural numbers.
Русский
Эквивалентно характеристикам сходимости к верхнему пределу в ENat через нижнюю грань на натуральных числах.
LaTeX
$$$$\\forall \\alpha,\\; l: Filter \\alpha,\\; f: \\alpha \\to \\mathbb{N}_{\\infty} \\;\n \\text{Tendsto } f\\ l\\ (\\mathcal{N}_{\\top}) \\iff \\forall n \\in \\mathbb{N},\\; \\forall^\\infty a \\in l,\\; n < f(a).$$$$
Lean4
theorem enatSub {α : Type*} {l : Filter α} {f g : α → ℕ∞} {a b : ℕ∞} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b))
(h : a ≠ ⊤ ∨ b ≠ ⊤) : Tendsto (fun x ↦ f x - g x) l (𝓝 (a - b)) :=
(ENat.continuousAt_sub h).tendsto.comp (hf.prodMk_nhds hg)
