English
If a sequence f: ℕ → Y converges to y in Y, then there is a continuous map from the one-point compactification of ℕ to Y that extends f and sends the point at infinity to y.
Русский
Если последовательность f: ℕ → Y сходится к y в Y, то существует непрерывное отображение из однопунктовой компактфикации ℕ в Y, которое продолжает f и отправляет бесконечность в y.
LaTeX
$$$\\exists \\phi: \\mathrm{ContinuousMap}(\\mathrm{OnePoint}(\\mathbb{N}), Y)$ с тем, что $\\phi|_{\\mathbb{N}} = f$ и $\\phi(\\infty) = y$ при $\\mathrm{Tendsto}(f)_{\\mathrm{atTop}}(\\mathcal{N}(y))$.$$
Lean4
/-- A constructor for continuous maps out of the one point compactification of `ℕ`, given a
sequence and a limit value at infinity.
-/
def continuousMapMkNat {Y : Type*} [TopologicalSpace Y] (f : ℕ → Y) (y : Y) (h : Tendsto f atTop (𝓝 y)) :
C(OnePoint ℕ, Y) :=
continuousMapMkDiscrete f y (by rwa [Nat.cofinite_eq_atTop])
