- 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
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.