Homeomorphisms #
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αtoβ. 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.
@[nolint]
structure
homeomorph
(α : Type u_5)
(β : Type u_6)
[topological_space α]
[topological_space β] :
Type (max u_5 u_6)
- 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
@[instance]
def
homeomorph.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
has_coe_to_fun (α ≃ₜ β)
@[simp]
theorem
homeomorph.homeomorph_mk_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(a : α ≃ β)
(b : continuous a.to_fun . "continuity'")
(c : continuous a.inv_fun . "continuity'") :
⇑{to_equiv := a, continuous_to_fun := b, continuous_inv_fun := c} = ⇑a
@[simp]
theorem
homeomorph.coe_to_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
def
homeomorph.symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
β ≃ₜ α
Inverse of a homeomorphism.
Equations
- h.symm = {to_equiv := h.to_equiv.symm, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.simps.apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
α → β
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
homeomorph.simps.symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
β → α
See Note [custom simps projection]
Equations
theorem
homeomorph.to_equiv_injective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
@[ext]
theorem
homeomorph.ext
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{h h' : α ≃ₜ β}
(H : ∀ (x : α), ⇑h x = ⇑h' x) :
h = h'
Identity map as a homeomorphism.
Equations
- homeomorph.refl α = {to_equiv := equiv.refl α, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
def
homeomorph.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h₁ : α ≃ₜ β)
(h₂ : β ≃ₜ γ) :
α ≃ₜ γ
Composition of two homeomorphisms.
Equations
- h₁.trans h₂ = {to_equiv := h₁.to_equiv.trans h₂.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.homeomorph_mk_coe_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(a : α ≃ β)
(b : continuous a.to_fun . "continuity'")
(c : continuous a.inv_fun . "continuity'") :
⇑({to_equiv := a, continuous_to_fun := b, continuous_inv_fun := c}.symm) = ⇑(a.symm)
@[simp]
theorem
homeomorph.refl_symm
{α : Type u_1}
[topological_space α] :
(homeomorph.refl α).symm = homeomorph.refl α
theorem
homeomorph.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.continuous_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
continuous ⇑(h.symm)
@[simp]
theorem
homeomorph.apply_symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(x : β) :
@[simp]
theorem
homeomorph.symm_apply_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(x : α) :
theorem
homeomorph.bijective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.injective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.surjective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
def
homeomorph.change_inv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α ≃ₜ β)
(g : β → α)
(hg : function.right_inverse g ⇑f) :
α ≃ₜ β
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 := _}
@[simp]
theorem
homeomorph.symm_comp_self
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[simp]
theorem
homeomorph.self_comp_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[simp]
theorem
homeomorph.range_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.image_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.preimage_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[simp]
theorem
homeomorph.image_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(s : set β) :
@[simp]
theorem
homeomorph.preimage_image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(s : set α) :
theorem
homeomorph.inducing
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.induced_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
topological_space.induced ⇑h _inst_2 = _inst_1
theorem
homeomorph.quotient_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.coinduced_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
topological_space.coinduced ⇑h _inst_1 = _inst_2
theorem
homeomorph.embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
def
homeomorph.of_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
(hf : embedding f) :
Homeomorphism given an embedding.
Equations
- homeomorph.of_embedding f hf = {to_equiv := {to_fun := (equiv.of_injective f _).to_fun, inv_fun := (equiv.of_injective f _).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
homeomorph.second_countable_topology
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[topological_space.second_countable_topology β]
(h : α ≃ₜ β) :
theorem
homeomorph.compact_image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{s : set α}
(h : α ≃ₜ β) :
is_compact (⇑h '' s) ↔ is_compact s
theorem
homeomorph.compact_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{s : set β}
(h : α ≃ₜ β) :
is_compact (⇑h ⁻¹' s) ↔ is_compact s
theorem
homeomorph.dense_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[simp]
theorem
homeomorph.is_open_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
{s : set β} :
@[simp]
theorem
homeomorph.is_open_image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
{s : set α} :
@[simp]
theorem
homeomorph.is_closed_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
{s : set β} :
@[simp]
theorem
homeomorph.is_closed_image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
{s : set α} :
theorem
homeomorph.preimage_closure
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(s : set β) :
theorem
homeomorph.image_closure
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(s : set α) :
theorem
homeomorph.is_open_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.is_closed_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
theorem
homeomorph.closed_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[simp]
theorem
homeomorph.map_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(x : α) :
theorem
homeomorph.symm_map_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(x : α) :
theorem
homeomorph.nhds_eq_comap
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(x : α) :
@[simp]
theorem
homeomorph.comap_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(y : β) :
def
homeomorph.homeomorph_of_continuous_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ β)
(h₁ : continuous ⇑e)
(h₂ : is_open_map ⇑e) :
α ≃ₜ β
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 := _}
@[simp]
theorem
homeomorph.comp_continuous_on_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
(f : γ → α)
(s : set γ) :
continuous_on (⇑h ∘ f) s ↔ continuous_on f s
@[simp]
theorem
homeomorph.comp_continuous_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
{f : γ → α} :
continuous (⇑h ∘ f) ↔ continuous f
@[simp]
theorem
homeomorph.comp_continuous_iff'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
{f : β → γ} :
continuous (f ∘ ⇑h) ↔ continuous f
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 := _}
def
homeomorph.sum_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(h₁ : α ≃ₜ β)
(h₂ : γ ≃ₜ δ) :
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 := _}
def
homeomorph.prod_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(h₁ : α ≃ₜ β)
(h₂ : γ ≃ₜ δ) :
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 := _}
@[simp]
theorem
homeomorph.prod_congr_symm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(h₁ : α ≃ₜ β)
(h₂ : γ ≃ₜ δ) :
(h₁.prod_congr h₂).symm = h₁.symm.prod_congr h₂.symm
@[simp]
theorem
homeomorph.coe_prod_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(h₁ : α ≃ₜ β)
(h₂ : γ ≃ₜ δ) :
def
homeomorph.prod_comm
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β] :
α × β is homeomorphic to β × α.
Equations
- homeomorph.prod_comm α β = {to_equiv := equiv.prod_comm α β, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.prod_comm_symm
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β] :
(homeomorph.prod_comm α β).symm = homeomorph.prod_comm β α
@[simp]
theorem
homeomorph.coe_prod_comm
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β] :
⇑(homeomorph.prod_comm α β) = prod.swap
def
homeomorph.prod_assoc
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
[topological_space α]
[topological_space β]
[topological_space γ] :
(α × β) × γ is homeomorphic to α × (β × γ).
Equations
- homeomorph.prod_assoc α β γ = {to_equiv := equiv.prod_assoc α β γ, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
α × {*} is homeomorphic to α.
Equations
- homeomorph.prod_punit α = {to_equiv := equiv.prod_punit α, continuous_to_fun := _, continuous_inv_fun := _}
{*} × α is homeomorphic to α.
Equations
@[simp]
ulift α is homeomorphic to α.
Equations
- homeomorph.ulift = {to_equiv := equiv.ulift α, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.sum_prod_distrib
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ] :
(α ⊕ β) × γ 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
def
homeomorph.prod_sum_distrib
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ] :
α × (β ⊕ γ) 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 γ α)))
def
homeomorph.sigma_prod_distrib
{β : Type u_2}
[topological_space β]
{ι : Type u_5}
{σ : ι → Type u_6}
[Π (i : ι), topological_space (σ i)] :
(Σ 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
def
homeomorph.image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β)
(s : set α) :
A subset of a topological space is homeomorphic to its image under a homeomorphism.