English
For a discrete space X and a map f: X → Y with limit y at infinity along cofinite, there is a continuous map from OnePoint X to Y extending f with value y at ∞.
Русский
Для дискретного пространства X и отображения f: X → Y с пределом y при бесконечности, существует непрерывное отображение OnePoint X → Y, продолжающее f и отправляющее ∞ в y.
LaTeX
$$$f : X \to Y$, $y \in Y$, $h: Tendsto f \text{ cofinite } (\mathcal{N} y) \Rightarrow C(OnePoint X, Y)$$$
Lean4
/-- A constructor for continuous maps out of a one point compactification of a discrete space, given a
map from the underlying space and a limit value at infinity.
-/
def continuousMapMkDiscrete {Y : Type*} [TopologicalSpace Y] [DiscreteTopology X] (f : X → Y) (y : Y)
(h : Tendsto f cofinite (𝓝 y)) : C(OnePoint X, Y) :=
continuousMapMk ⟨f, continuous_of_discreteTopology⟩ y (by simpa [cocompact_eq_cofinite])
