English
If the union of the open cover equals the whole space, the glueing of the open cover is homeomorphic to the original space.
Русский
Если объединение открытых множеств равно всей пространству, то склейка открытого покрытия гомеоморфна оригинальному пространству.
LaTeX
$$openCoverGlueHomeo(h) : (ofOpenSubsets U).toGlueData.glued ≃ₜ α$$
Lean4
/-- The gluing of an open cover is homeomorphic to the original space. -/
def openCoverGlueHomeo (h : ⋃ i, (U i : Set α) = Set.univ) : (ofOpenSubsets U).toGlueData.glued ≃ₜ α :=
Equiv.toHomeomorphOfContinuousOpen
(Equiv.ofBijective (fromOpenSubsetsGlue U)
⟨fromOpenSubsetsGlue_injective U, Set.range_eq_univ.mp ((range_fromOpenSubsetsGlue U).symm ▸ h)⟩)
(fromOpenSubsetsGlue U).hom.2 (fromOpenSubsetsGlue_isOpenMap U)
