English
Let e be a homeomorphism between X and Y. Then it induces an open partial homeomorphism on the whole spaces by using the same map, with source = univ and target = univ.
Русский
Пусть e — гомеоморфизм между X и Y. Тогда он порождает открытый частичный гомеоморфизм на всём пространствах, используя ту же карту, с source = univ и target = univ.
LaTeX
$$$\text{Let } e: X \simeq_{t} Y. \text{ Then } E: OpenPartialHomeomorph\,X\,Y \text{ with } \operatorname{source}(E)=\operatorname{univ}, \operatorname{target}(E)=\operatorname{univ} \text{ exists and is given by the usual extension.}$$$
Lean4
/-- A homeomorphism induces an open partial homeomorphism on the whole space -/
@[simps! (attr := mfld_simps) -fullyApplied]
def _root_.Homeomorph.toOpenPartialHomeomorph (e : X ≃ₜ Y) : OpenPartialHomeomorph X Y :=
e.toOpenPartialHomeomorphOfImageEq univ isOpen_univ univ <| by rw [image_univ, e.surjective.range_eq]
