English
A map that is a homeomorphism yields a bundled homeomorphism with underlying map f.
Русский
Отображение, являющееся гомеоморфизмом, порождает связанный гомеоморфизм, чья базовая функция равна этому отображению.
LaTeX
$$$\exists h : X \to Y,\; h = f$ и $h$ — гомеоморфизм; \\ \text{(то же, что } f \text{ является гомеоморфизмом)}$$$
Lean4
/-- Bundled homeomorphism constructed from a map that is a homeomorphism. -/
@[simps! toEquiv apply symm_apply]
noncomputable def homeomorph : X ≃ₜ Y where
continuous_toFun := hf.1
continuous_invFun := by
rw [← continuousOn_univ, ← hf.bijective.2.range_eq]
exact hf.isOpenMap.continuousOn_range_of_leftInverse (leftInverse_surjInv hf.bijective)
toEquiv := Equiv.ofBijective f hf.bijective
