English
Characterization of convergence in ENNReal via base neighborhoods: Tendsto to a is equivalent to eventual membership in Icc(a−ε, a+ε) for all ε>0.
Русский
Характеризация сходимости в ENNReal через базис окрестностей: сходимость к a эквивалентна eventually в Icc(a−ε, a+ε) для всех ε>0.
LaTeX
$$$\\operatorname{Tendsto}u f (\\mathcal{N}a) \\iff \\forall \\varepsilon>0, \\forall^f x, u(x) \\in Icc(a-\\varepsilon, a+\\varepsilon)$$$
Lean4
/-- Characterization of neighborhoods for `ℝ≥0∞` numbers. See also `tendsto_order`
for a version with strict inequalities. -/
protected theorem tendsto_nhds {f : Filter α} {u : α → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞) :
Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, u x ∈ Icc (a - ε) (a + ε) := by
simp only [nhds_of_ne_top ha, tendsto_iInf, tendsto_principal]
