@[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
theorem
homeomorph.coe_eq_to_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(a : α) :
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 := {to_fun := (equiv.refl α).to_fun, inv_fun := (equiv.refl α).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h₁ : α ≃ₜ β)
(h₂ : β ≃ₜ γ) :
α ≃ₜ γ
Composition of two homeomorphisms.
def
homeomorph.symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
β ≃ₜ α
Inverse of a homeomorphism.
@[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)
theorem
homeomorph.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[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 : α ≃ₜ β) :
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 : α) :
@[simp]
theorem
homeomorph.comap_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(y : β) :
theorem
homeomorph.nhds_eq_comap
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(x : α) :
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 := {to_fun := e.to_fun, inv_fun := e.inv_fun, left_inv := _, right_inv := _}, 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 := {to_fun := (equiv.set_congr h).to_fun, inv_fun := (equiv.set_congr h).inv_fun, left_inv := _, right_inv := _}, 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.
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 := {to_fun := (h₁.to_equiv.prod_congr h₂.to_equiv).to_fun, inv_fun := (h₁.to_equiv.prod_congr h₂.to_equiv).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.prod_comm
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β] :
α × β is homeomorphic to β × α.
Equations
- homeomorph.prod_comm α β = {to_equiv := {to_fun := (equiv.prod_comm α β).to_fun, inv_fun := (equiv.prod_comm α β).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
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 := {to_fun := (equiv.prod_assoc α β γ).to_fun, inv_fun := (equiv.prod_assoc α β γ).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
ulift α is homeomorphic to α.
Equations
- homeomorph.ulift = {to_equiv := {to_fun := equiv.ulift.to_fun, inv_fun := equiv.ulift.inv_fun, left_inv := _, right_inv := _}, 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