English
Let f: β → ENNReal with β nonempty and β directed such that f tends to 0 along atTop. Then f converges to 0 iff for every ε > 0 there exists N with f(n) ≤ ε for all n ≥ N.
Русский
Пусть f: β → ENNReal, β ненулевой и ориентирован так, что f стремится к 0 вдоль atTop. Тогда f сходится к 0 тогда и только тогда, когда для каждого ε > 0 существует N такой, что f(n) ≤ ε для всех n ≥ N.
LaTeX
$$$\\\\operatorname{Tendsto} f \\\\mathrm{atTop} \\\\,(\\\\mathit{nhds} \ 0) \\\\iff \\\\forall \\\\varepsilon > 0, \\\\exists N, \\\\forall n \\\\ge N, \\\\ f(n) \\\\le \\\\varepsilon.$$$
Lean4
protected theorem tendsto_atTop_zero [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞} :
Tendsto f atTop (𝓝 0) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε :=
.trans (atTop_basis.tendsto_iff nhds_zero_basis_Iic) (by simp only [true_and]; rfl)
