English
Extend a homeomorphism of spaces to a homeomorphism of their one-point compactifications.
Русский
Продлить гомеоморфизм пространств до гомеоморфизма их однопунктовых компактфикаций.
LaTeX
$$$\\text{OnePoint}.\\mathrm{onePointCongr} : (X \\simeq_{t} Y) \\to (\\mathrm{OnePoint}(X) \\simeq_{t} \\mathrm{OnePoint}(Y)).$$$
Lean4
/-- Extend a homeomorphism of topological spaces
to the homeomorphism of their one point compactifications. -/
@[simps]
def onePointCongr (h : X ≃ₜ Y) : OnePoint X ≃ₜ OnePoint Y
where
__ := h.toEquiv.withTopCongr
toFun := OnePoint.map h
invFun := OnePoint.map h.symm
continuous_toFun := continuous_map (map_continuous h) h.map_coclosedCompact.le
continuous_invFun := continuous_map (map_continuous h.symm) h.symm.map_coclosedCompact.le
