English
If f: β → ENNReal is antitone and β is nonempty with a finite limit, then Tendsto f atTop (nhds 0) is equivalent to: for every ε > 0, there exists n in β with f(n) ≤ ε.
Русский
Если f: β → ENNReal анти монотоне и β непустое, а предел конечен, то предел f при atTop к 0 эквивалентен тому, что для каждого ε > 0 существует n such that f(n) ≤ ε.
LaTeX
$$$\\\\text{Antitone } f \\\\Rightarrow \\\\operatorname{Tendsto} f \\\\mathrm{atTop} \\\\,(\\\\mathit{nhds} \ 0) \\\\iff \\\\forall \\\\varepsilon > 0, \\\\exists n \\\\in \\\\beta: f(n) \\\\le \\\\varepsilon.$$$
Lean4
theorem tendsto_atTop_zero_iff_le_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞}
(hf : Antitone f) : Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n ≤ ε :=
by
rw [ENNReal.tendsto_atTop_zero]
refine ⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩
· obtain ⟨n, hn⟩ := h ε hε
exact ⟨n, hn n le_rfl⟩
· obtain ⟨n, hn⟩ := h ε hε
exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩
