- 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
Composition of two homeomorphisms.
Inverse of a homeomorphism.
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.
If two sets are equal, then they are homeomorphic.
Sum of two homeomorphisms.
Product of two homeomorphisms.
α × β is homeomorphic to
β × α.
(α × β) × γ is homeomorphic to
α × (β × γ).
(α ⊕ β) × γ is homeomorphic to
α × γ ⊕ β × γ.
α × (β ⊕ γ) is homeomorphic to
α × β ⊕ α × γ.
(Σ i, σ i) × β is homeomorphic to
Σ i, (σ i × β).