- to_equiv : α ≃ β
- continuous_to_fun : continuous c.to_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous c.to_equiv.inv_fun . "continuity'"
Homeomorphism between α
and β
, also called topological isomorphism
Inverse of a homeomorphism.
Equations
- h.symm = {to_equiv := h.to_equiv.symm, continuous_to_fun := _, continuous_inv_fun := _}
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
See Note [custom simps projection]
Equations
Identity map as a homeomorphism.
Equations
- homeomorph.refl α = {to_equiv := equiv.refl α, continuous_to_fun := _, continuous_inv_fun := _}
Composition of two homeomorphisms.
Equations
- h₁.trans h₂ = {to_equiv := h₁.to_equiv.trans h₂.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
Change the homeomorphism f
to make the inverse function definitionally equal to g
.
Equations
- f.change_inv g hg = have this : g = ⇑(f.symm), from _, {to_equiv := {to_fun := ⇑f, inv_fun := g, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
If an bijective map e : α ≃ β
is continuous and open, then it is a homeomorphism.
Equations
- homeomorph.homeomorph_of_continuous_open e h₁ h₂ = {to_equiv := e, continuous_to_fun := h₁, continuous_inv_fun := _}
If two sets are equal, then they are homeomorphic.
Equations
- homeomorph.set_congr h = {to_equiv := equiv.set_congr h, continuous_to_fun := _, continuous_inv_fun := _}
Sum of two homeomorphisms.
Equations
- h₁.sum_congr h₂ = {to_equiv := h₁.to_equiv.sum_congr h₂.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
Product of two homeomorphisms.
Equations
- h₁.prod_congr h₂ = {to_equiv := h₁.to_equiv.prod_congr h₂.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
α × β
is homeomorphic to β × α
.
Equations
- homeomorph.prod_comm α β = {to_equiv := equiv.prod_comm α β, continuous_to_fun := _, continuous_inv_fun := _}
(α × β) × γ
is homeomorphic to α × (β × γ)
.
Equations
- homeomorph.prod_assoc α β γ = {to_equiv := equiv.prod_assoc α β γ, continuous_to_fun := _, continuous_inv_fun := _}
α × {*}
is homeomorphic to α
.
Equations
- homeomorph.prod_punit α = {to_equiv := equiv.prod_punit α, continuous_to_fun := _, continuous_inv_fun := _}
{*} × α
is homeomorphic to α
.
Equations
ulift α
is homeomorphic to α
.
Equations
- homeomorph.ulift = {to_equiv := equiv.ulift α, continuous_to_fun := _, continuous_inv_fun := _}
(α ⊕ β) × γ
is homeomorphic to α × γ ⊕ β × γ
.
Equations
- homeomorph.sum_prod_distrib = (homeomorph.homeomorph_of_continuous_open (equiv.sum_prod_distrib α β γ).symm homeomorph.sum_prod_distrib._proof_1 homeomorph.sum_prod_distrib._proof_2).symm
α × (β ⊕ γ)
is homeomorphic to α × β ⊕ α × γ
.
Equations
- homeomorph.prod_sum_distrib = (homeomorph.prod_comm α (β ⊕ γ)).trans (homeomorph.sum_prod_distrib.trans ((homeomorph.prod_comm β α).sum_congr (homeomorph.prod_comm γ α)))
(Σ i, σ i) × β
is homeomorphic to Σ i, (σ i × β)
.
Equations
- homeomorph.sigma_prod_distrib = (homeomorph.homeomorph_of_continuous_open (equiv.sigma_prod_distrib σ β).symm homeomorph.sigma_prod_distrib._proof_1 homeomorph.sigma_prod_distrib._proof_2).symm
A subset of a topological space is homeomorphic to its image under a homeomorphism.