English
Let f: β → ENNReal be defined on a nonempty index set β with a finite limit a ∈ ENNReal (i.e., a ≠ ∞) along the directed set atTop. Then f converges to a along atTop precisely when, for every ε > 0, there exists N such that for all n ≥ N we have f(n) ∈ [a − ε, a + ε], i.e., f(n) lies in the closed interval Icc(a − ε, a + ε).
Русский
Пусть f: β → ℝ≥0∞ определена на ненулевом индексе β и имеет конечную пределa a ∈ ℝ≥0∞ (то есть a ≠ ∞) вдоль направленного множителя atTop. Тогда f сходится к a по atTop тогда и только тогда, для каждого ε > 0 существует N, такое что для всех n ≥ N выполняется f(n) ∈ [a − ε, a + ε], то есть f(n) лежит в замкнутом интервале Icc(a − ε, a + ε).
LaTeX
$$$\\\\operatorname{Tendsto} f \\, \mathrm{atTop} \, (\\\\mathit{nhds} \ a) \\\\iff \\\\forall \\\\varepsilon > 0, \\\\exists N, \\\\forall n \\\\ge N, \\\\ f(n) \\\\in \\\\mathrm{Icc}(a - \\\\varepsilon, a + \\\\varepsilon).$$$
Lean4
protected theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞) :
Tendsto f atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε) :=
.trans (atTop_basis.tendsto_iff (hasBasis_nhds_of_ne_top ha)) (by simp only [true_and]; rfl)
