THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 self.to_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous self.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
α × (β × γ).
β have a unique element, then
α ≃ₜ β.
β₁ i is homeomorphic to
β₂ i, then
Π i, β₁ i is homeomorphic to
Π i, β₂ i.
(α ⊕ β) × γ is homeomorphic to
α × γ ⊕ β × γ.
α × (β ⊕ γ) is homeomorphic to
α × β ⊕ α × γ.
(Σ i, σ i) × β is homeomorphic to
Σ i, (σ i × β).
Homeomorphism between dependent functions
Π i : fin 2, α i and
α 0 × α 1.
A subset of a topological space is homeomorphic to its image under a homeomorphism.
The topological space
Π i, β i can be split as a product by separating the indices in ι
depending on whether they satisfy a predicate p or not.
A product of topological spaces can be split as the binary product of one of the spaces and the product of all the remaining spaces.
A product of copies of a topological space can be split as the binary product of one copy and the product of all the remaining copies.
An inducing equiv between topological spaces is a homeomorphism.
Continuous equivalences from a compact space to a T2 space are homeomorphisms.
This is not true when T2 is weakened to T1