English
For a Hausdorff space Y, continuous maps from the one-point nat compactification to Y correspond bijectively to the set of sequences in Y that converge (to some limit).
Русский
Для Гаусдорфового пространства Y непрерывные отображения из однопунктовой компактфикации ℕ в Y образуют биектически сопряжённое соответствие с множеством последовательностей в Y, сходящихся к некоторому пределу.
LaTeX
$$$\\mathrm{ContinuousMap}(\\mathrm{OnePoint}(\\mathbb{N}), Y) \\simeq \\{ f: \\mathbb{N} \\to Y \\;\\middle|\\; \\exists L, \\operatorname{Tendsto}(f)_{\\mathrm{atTop}}(\\mathcal{N}(L))\\},$ где $Y$ удовлетворяет свойству T_2.$$
Lean4
/-- Continuous maps out of the one point compactification of `ℕ` to a Hausdorff space `Y` correspond
bijectively to convergent sequences in `Y`.
-/
noncomputable def continuousMapNatEquiv (Y : Type*) [TopologicalSpace Y] [T2Space Y] :
C(OnePoint ℕ, Y) ≃ { f : ℕ → Y // ∃ L, Tendsto (f ·) atTop (𝓝 L) } := by
refine
(continuousMapDiscreteEquiv ℕ Y).trans
{ toFun := fun ⟨f, hf⟩ ↦ ⟨f, by rwa [← Nat.cofinite_eq_atTop]⟩
invFun := fun ⟨f, hf⟩ ↦ ⟨f, by rwa [Nat.cofinite_eq_atTop]⟩ }
