English
Given a continuous map f: X → Y and a limit y ∈ Y with Tendsto f to y along coclosedCompact X, there exists a continuous extension F: OnePoint X → Y with F|X = f and F(∞) = y.
Русский
Пусть f: X → Y непрерывна и существует предел y при пределе к бесконечности; тогда существует непрерывное продолжение F: OnePoint X → Y с F|X = f и F(∞) = y.
LaTeX
$$$\exists F: C(OnePoint X, Y)$, $F\restriction_X = f$ and $F(\infty) = y$ provided $f$ is continuous on X and $Tendsto f (coclosedCompact X) (\mathcal{N} y)$.$$
Lean4
/-- A constructor for continuous maps out of a one point compactification, given a continuous map from
the underlying space and a limit value at infinity.
-/
def continuousMapMk {Y : Type*} [TopologicalSpace Y] (f : C(X, Y)) (y : Y) (h : Tendsto f (coclosedCompact X) (𝓝 y)) :
C(OnePoint X, Y) where
toFun x := x.elim y f
continuous_toFun := by
rw [continuous_iff]
refine ⟨h, f.continuous⟩
