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 self.to_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous self.to_equiv.inv_fun . "continuity'"
Homeomorphism between α and β, also called topological isomorphism
Instances for homeomorph
- homeomorph.has_sizeof_inst
- homeomorph.has_coe_to_fun
- homeomorph.continuous_map.has_coe
@[protected, instance]
def
homeomorph.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
has_coe_to_fun (α ≃ₜ β) (λ (_x : α ≃ₜ β), α → β)
@[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
@[protected]
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
@[simp]
theorem
homeomorph.coe_to_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[simp]
theorem
homeomorph.coe_symm_to_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
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'
@[protected]
Identity map as a homeomorphism.
Equations
- homeomorph.refl α = {to_equiv := equiv.refl α, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
@[protected]
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.trans_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h₁ : α ≃ₜ β)
(h₂ : β ≃ₜ γ)
(a : α) :
@[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 α
@[protected, continuity]
theorem
homeomorph.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[protected, continuity]
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 : α) :
@[simp]
theorem
homeomorph.self_trans_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
h.trans h.symm = homeomorph.refl α
@[simp]
theorem
homeomorph.symm_trans_self
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
h.symm.trans h = homeomorph.refl β
@[protected]
theorem
homeomorph.bijective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[protected]
theorem
homeomorph.injective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[protected]
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 α) :
@[protected]
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
@[protected]
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
@[protected]
theorem
homeomorph.embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
noncomputable
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 := equiv.of_injective f _, continuous_to_fun := _, continuous_inv_fun := _}
@[protected]
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
@[simp]
theorem
homeomorph.comap_cocompact
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[simp]
theorem
homeomorph.map_cocompact
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
filter.map ⇑h (filter.cocompact α) = filter.cocompact β
@[protected]
theorem
homeomorph.compact_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[compact_space α]
(h : α ≃ₜ β) :
@[protected]
theorem
homeomorph.t0_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[t0_space α]
(h : α ≃ₜ β) :
t0_space β
@[protected]
theorem
homeomorph.t1_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[t1_space α]
(h : α ≃ₜ β) :
t1_space β
@[protected]
theorem
homeomorph.t2_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[t2_space α]
(h : α ≃ₜ β) :
t2_space β
@[protected]
theorem
homeomorph.t3_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[t3_space α]
(h : α ≃ₜ β) :
t3_space β
@[protected]
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 α} :
@[protected]
theorem
homeomorph.is_open_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[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 α} :
@[protected]
theorem
homeomorph.is_closed_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[protected]
theorem
homeomorph.open_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[protected]
theorem
homeomorph.closed_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β) :
@[protected]
theorem
homeomorph.normal_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[normal_space α]
(h : α ≃ₜ β) :
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.preimage_interior
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(s : set β) :
theorem
homeomorph.image_interior
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(s : set α) :
theorem
homeomorph.preimage_frontier
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(h : α ≃ₜ β)
(s : set β) :
theorem
has_compact_support.comp_homeomorph
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{M : Type u_3}
[has_zero M]
{f : β → M}
(hf : has_compact_support f)
(φ : α ≃ₜ β) :
has_compact_support (f ∘ ⇑φ)
theorem
has_compact_mul_support.comp_homeomorph
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{M : Type u_3}
[has_one M]
{f : β → M}
(hf : has_compact_mul_support f)
(φ : α ≃ₜ β) :
has_compact_mul_support (f ∘ ⇑φ)
@[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
theorem
homeomorph.comp_continuous_at_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
(f : γ → α)
(x : γ) :
continuous_at (⇑h ∘ f) x ↔ continuous_at f x
theorem
homeomorph.comp_continuous_at_iff'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
(f : β → γ)
(x : α) :
continuous_at (f ∘ ⇑h) x ↔ continuous_at f (⇑h x)
theorem
homeomorph.comp_continuous_within_at_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
(f : γ → α)
(s : set γ)
(x : γ) :
continuous_within_at f s x ↔ continuous_within_at (⇑h ∘ f) s x
@[simp]
theorem
homeomorph.comp_is_open_map_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
{f : γ → α} :
is_open_map (⇑h ∘ f) ↔ is_open_map f
@[simp]
theorem
homeomorph.comp_is_open_map_iff'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(h : α ≃ₜ β)
{f : β → γ} :
is_open_map (f ∘ ⇑h) ↔ is_open_map 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]
@[simp]
theorem
homeomorph.homeomorph_of_unique_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[unique α]
[unique β]
(ᾰ : α) :
⇑(homeomorph.homeomorph_of_unique α β) ᾰ = (equiv.equiv_of_unique α β).to_fun ᾰ
def
homeomorph.homeomorph_of_unique
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[unique α]
[unique β] :
α ≃ₜ β
If both α and β have a unique element, then α ≃ₜ β.
Equations
- homeomorph.homeomorph_of_unique α β = {to_equiv := {to_fun := (equiv.equiv_of_unique α β).to_fun, inv_fun := (equiv.equiv_of_unique α β).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.homeomorph_of_unique_symm_apply
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[unique α]
[unique β]
(ᾰ : β) :
⇑((homeomorph.homeomorph_of_unique α β).symm) ᾰ = (equiv.equiv_of_unique α β).inv_fun ᾰ
@[simp]
theorem
homeomorph.Pi_congr_right_to_equiv
{ι : Type u_1}
{β₁ : ι → Type u_2}
{β₂ : ι → Type u_3}
[Π (i : ι), topological_space (β₁ i)]
[Π (i : ι), topological_space (β₂ i)]
(F : Π (i : ι), β₁ i ≃ₜ β₂ i) :
(homeomorph.Pi_congr_right F).to_equiv = equiv.Pi_congr_right (λ (i : ι), (F i).to_equiv)
@[simp]
theorem
homeomorph.Pi_congr_right_apply
{ι : Type u_1}
{β₁ : ι → Type u_2}
{β₂ : ι → Type u_3}
[Π (i : ι), topological_space (β₁ i)]
[Π (i : ι), topological_space (β₂ i)]
(F : Π (i : ι), β₁ i ≃ₜ β₂ i)
(H : Π (a : ι), (λ (i : ι), β₁ i) a)
(a : ι) :
⇑(homeomorph.Pi_congr_right F) H a = ⇑(F a) (H a)
def
homeomorph.Pi_congr_right
{ι : Type u_1}
{β₁ : ι → Type u_2}
{β₂ : ι → Type u_3}
[Π (i : ι), topological_space (β₁ i)]
[Π (i : ι), topological_space (β₂ i)]
(F : Π (i : ι), β₁ i ≃ₜ β₂ i) :
(Π (i : ι), β₁ i) ≃ₜ Π (i : ι), β₂ i
If each β₁ i is homeomorphic to β₂ i, then Π i, β₁ i is homeomorphic to Π i, β₂ i.
Equations
- homeomorph.Pi_congr_right F = {to_equiv := equiv.Pi_congr_right (λ (i : ι), (F i).to_equiv), continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.Pi_congr_right_symm
{ι : Type u_1}
{β₁ : ι → Type u_2}
{β₂ : ι → Type u_3}
[Π (i : ι), topological_space (β₁ i)]
[Π (i : ι), topological_space (β₂ i)]
(F : Π (i : ι), β₁ i ≃ₜ β₂ i) :
(homeomorph.Pi_congr_right F).symm = homeomorph.Pi_congr_right (λ (i : ι), (F i).symm)
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.fun_unique
(ι : Type u_1)
(α : Type u_2)
[unique ι]
[topological_space α] :
(ι → α) ≃ₜ α
If ι has a unique element, then ι → α is homeomorphic to α.
Equations
- homeomorph.fun_unique ι α = {to_equiv := equiv.fun_unique ι α _inst_5, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.fun_unique_apply
(ι : Type u_1)
(α : Type u_2)
[unique ι]
[topological_space α] :
@[simp]
theorem
homeomorph.fun_unique_symm_apply
(ι : Type u_1)
(α : Type u_2)
[unique ι]
[topological_space α] :
⇑((homeomorph.fun_unique ι α).symm) = λ (x : α) (b : ι), x
@[simp]
theorem
homeomorph.pi_fin_two_symm_apply
(α : fin 2 → Type u)
[Π (i : fin 2), topological_space (α i)] :
⇑((homeomorph.pi_fin_two α).symm) = λ (p : α 0 × α 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
Homeomorphism between dependent functions Π i : fin 2, α i and α 0 × α 1.
Equations
- homeomorph.pi_fin_two α = {to_equiv := pi_fin_two_equiv α, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.pi_fin_two_apply
(α : fin 2 → Type u)
[Π (i : fin 2), topological_space (α i)] :
⇑(homeomorph.pi_fin_two α) = λ (f : Π (i : fin 2), α i), (f 0, f 1)
@[simp]
theorem
homeomorph.fin_two_arrow_apply
{α : Type u_1}
[topological_space α] :
⇑homeomorph.fin_two_arrow = λ (f : fin 2 → α), (f 0, f 1)
@[simp]
Homeomorphism between α² = fin 2 → α and α × α.
Equations
- homeomorph.fin_two_arrow = {to_equiv := fin_two_arrow_equiv α, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.image_apply_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β)
(s : set α)
(x : ↥s) :
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.
Equations
- e.image s = {to_equiv := e.to_equiv.image s, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.set.univ_apply
(α : Type u_1)
[topological_space α] :
⇑(homeomorph.set.univ α) = coe
set.univ α is homeomorphic to α.
Equations
- homeomorph.set.univ α = {to_equiv := equiv.set.univ α, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.set.univ_symm_apply_coe
(α : Type u_1)
[topological_space α]
(a : α) :
↑(⇑((homeomorph.set.univ α).symm) a) = a
@[simp]
theorem
homeomorph.set.prod_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α)
(t : set β)
(x : {c // s c.fst ∧ t c.snd}) :
@[simp]
theorem
homeomorph.set.prod_symm_apply_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α)
(t : set β)
(x : {a // s a} × {b // t b}) :
def
homeomorph.set.prod
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α)
(t : set β) :
s ×ˢ t is homeomorphic to s × t.
Equations
- homeomorph.set.prod s t = {to_equiv := equiv.set.prod s t, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
equiv.to_homeomorph_of_inducing_symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α ≃ β)
(hf : inducing ⇑f)
(ᾰ : β) :
⇑((f.to_homeomorph_of_inducing hf).symm) ᾰ = f.inv_fun ᾰ
@[simp]
theorem
equiv.to_homeomorph_of_inducing_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α ≃ β)
(hf : inducing ⇑f)
(ᾰ : α) :
⇑(f.to_homeomorph_of_inducing hf) ᾰ = f.to_fun ᾰ
def
equiv.to_homeomorph_of_inducing
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α ≃ β)
(hf : inducing ⇑f) :
α ≃ₜ β
An inducing equiv between topological spaces is a homeomorphism.
Equations
- f.to_homeomorph_of_inducing hf = {to_equiv := {to_fun := f.to_fun, inv_fun := f.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
continuous.continuous_symm_of_equiv_compact_to_t2
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[compact_space α]
[t2_space β]
{f : α ≃ β}
(hf : continuous ⇑f) :
continuous ⇑(f.symm)
def
continuous.homeo_of_equiv_compact_to_t2
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[compact_space α]
[t2_space β]
{f : α ≃ β}
(hf : continuous ⇑f) :
α ≃ₜ β
Continuous equivalences from a compact space to a T2 space are homeomorphisms.
This is not true when T2 is weakened to T1
(see continuous.homeo_of_equiv_compact_to_t2.t1_counterexample).
Equations
- hf.homeo_of_equiv_compact_to_t2 = {to_equiv := {to_fun := f.to_fun, inv_fun := f.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := hf, continuous_inv_fun := _}
@[simp]
theorem
continuous.homeo_of_equiv_compact_to_t2_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[compact_space α]
[t2_space β]
{f : α ≃ β}
(hf : continuous ⇑f)
(ᾰ : α) :
⇑(hf.homeo_of_equiv_compact_to_t2) ᾰ = f.to_fun ᾰ
@[simp]
theorem
continuous.homeo_of_equiv_compact_to_t2_symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[compact_space α]
[t2_space β]
{f : α ≃ β}
(hf : continuous ⇑f)
(ᾰ : β) :
⇑(hf.homeo_of_equiv_compact_to_t2.symm) ᾰ = f.inv_fun ᾰ