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.homeomorphOfContinuousOpen: A continuous bijection that is an open map is a homeomorphism.
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- continuous_toFun : Continuous s.toFun
The forward map of a homeomorphism is a continuous function.
- continuous_invFun : Continuous s.invFun
The inverse map of a homeomorphism is a continuous function.
β, also called topological isomorphism
Equiv.piCongrLeft as a homeomorphism: this is the natural homeomorphism
Π i, β (e i) ≃ₜ Π j, β j obtained from a bijection
ι ≃ ι'.
Equiv.piCongrRight as a homeomorphism: this is the natural homeomorphism
Π i, β₁ i ≃ₜ Π j, β₂ i obtained from homeomorphisms
β₁ i ≃ₜ β₂ i for each
Equiv.piCongr as a homeomorphism: this is the natural homeomorphism
Π i₁, β₁ i ≃ₜ Π i₂, β₂ i₂ obtained from a bijection
ι₁ ≃ ι₂ and homeomorphisms
β₁ i₁ ≃ₜ β₂ (e i₁) for each
i₁ : ι₁.
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.
Continuous equivalences from a compact space to a T2 space are homeomorphisms.
This is not true when T2 is weakened to T1