This file defines homeomorphisms between two topological spaces. They are bijections with both
directions continuous. We denote homeomorphisms with the notation
Main definitions #
homeomorph α β: The type of homeomorphisms from
β. This type can be denoted using the following notation:
α ≃ₜ β.
Main results #
- Pretty much every topological property is preserved under homeomorphisms.
homeomorph.homeomorph_of_continuous_open: A continuous bijection that is an open map is a homeomorphism.
- to_equiv : α ≃ β
- continuous_to_fun : continuous c.to_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous c.to_equiv.inv_fun . "continuity'"
β, also called topological isomorphism
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Composition of two homeomorphisms.
Change the homeomorphism
f to make the inverse function definitionally equal to
Homeomorphism given an embedding.
If an bijective map
e : α ≃ β is continuous and open, then it is a homeomorphism.
Sum of two homeomorphisms.
Product of two homeomorphisms.
(α × β) × γ is homeomorphic to
α × (β × γ).
(α ⊕ β) × γ is homeomorphic to
α × γ ⊕ β × γ.
α × (β ⊕ γ) is homeomorphic to
α × β ⊕ α × γ.
(Σ i, σ i) × β is homeomorphic to
Σ i, (σ i × β).
A subset of a topological space is homeomorphic to its image under a homeomorphism.