English
If a sequence f: α → β tends to b along atTop in a directed NoMaxOrder setting, then for every ε > 0 there exists N with the property that for all n > N, ‖f(n) − b‖ < ε.
Русский
Если последовательность f: α → β стремится к b по atTop в условиях отсутствия максимального элемента, то для каждого ε > 0 существует N, такое что для всех n > N выполняется ‖f(n) − b‖ < ε.
LaTeX
$$$Tendsto\\,f\\,atTop\\,(\\mathcal{N} b)\\;\\Longleftrightarrow\\; \\forall \\epsilon>0,\\; \\exists N,\\; \\forall n,\\ N < n \\Rightarrow \\|f(n)-b\\|<\\epsilon$$$
Lean4
/-- A variant of `NormedAddCommGroup.tendsto_atTop` that
uses `∃ N, ∀ n > N, ...` rather than `∃ N, ∀ n ≥ N, ...`
-/
theorem tendsto_atTop' [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α] {β : Type*}
[SeminormedAddCommGroup β] {f : α → β} {b : β} :
Tendsto f atTop (𝓝 b) ↔ ∀ ε, 0 < ε → ∃ N, ∀ n, N < n → ‖f n - b‖ < ε :=
(atTop_basis_Ioi.tendsto_iff Metric.nhds_basis_ball).trans (by simp [dist_eq_norm])
