English
Let α be a directed nonempty index set and β be a normed additive group. A function f: α → β tends to b along atTop if and only if for every ε > 0 there exists N such that for all n with N ≤ n, we have ‖f(n) − b‖ < ε.
Русский
Пусть α — ненулевой направленный индексный множество, β — нормированная аддитивная группа, и f: α → β. Тогда f нулевой предел вдоль atTop эквивалентен тому, что для любого ε > 0 существует N, такое что для всех n с N ≤ n выполняется ‖f(n) − b‖ < ε.
LaTeX
$$$Tendsto\,f\,atTop\\,(\\mathcal{N} b)\\;\\Longleftrightarrow\\; \\forall \\epsilon>0,\\; \\exists N,\\; \\forall n,\\ N \\le n \\Rightarrow \\|f(n)-b\\|<\\epsilon$$$
Lean4
/-- A restatement of `MetricSpace.tendsto_atTop` in terms of the norm. -/
theorem tendsto_atTop [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] {β : Type*} [SeminormedAddCommGroup β]
{f : α → β} {b : β} : Tendsto f atTop (𝓝 b) ↔ ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → ‖f n - b‖ < ε :=
(atTop_basis.tendsto_iff Metric.nhds_basis_ball).trans (by simp [dist_eq_norm])
