English
If f: α→X with α nonempty and α well-ordered by ≤ with a top element, then f tends to x along atTop if and only if for every open set U containing x there exists N such that f(n) ∈ U for all n ≥ N.
Русский
Пусть f: α→X, α ненулевой и пронумерован сверху; тогда f стремится к x вдоль atTop тогда и только тогда для каждого открытого множества U, содержащего x существует N такое, что для всех n ≥ N, f(n) ∈ U.
LaTeX
$$$\\text{Tendsto } f\\ atTop\\ (\\mathcal N_x) \\iff \\forall U,\\ x\\in U \\land IsOpen(U) \\Rightarrow \\exists N, \\forall n\\, (n ≥ N) \\Rightarrow f(n) ∈ U.$$$
Lean4
theorem tendsto_atTop_nhds [Nonempty α] [SemilatticeSup α] {f : α → X} :
Tendsto f atTop (𝓝 x) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U :=
(atTop_basis.tendsto_iff (nhds_basis_opens x)).trans <| by simp only [and_imp, true_and, mem_Ici]
