# mathlib3documentation

topology.homeomorph

# Homeomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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)  :
Type (max u_5 u_6)

Homeomorphism between `α` and `β`, also called topological isomorphism

Instances for `homeomorph`
@[protected, instance]
def homeomorph.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
has_coe_to_fun ≃ₜ β) (λ (_x : α ≃ₜ β), α β)
Equations
@[simp]
theorem homeomorph.homeomorph_mk_coe {α : Type u_1} {β : Type u_2} (a : α β) (b : . "continuity'") (c : . "continuity'") :
@[protected]
def homeomorph.symm {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
β ≃ₜ α

Inverse of a homeomorphism.

Equations
def homeomorph.simps.apply {α : Type u_1} {β : Type u_2} (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} (h : α ≃ₜ β) :
β α
Equations
@[simp]
theorem homeomorph.coe_to_equiv {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.coe_symm_to_equiv {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
theorem homeomorph.to_equiv_injective {α : Type u_1} {β : Type u_2}  :
@[ext]
theorem homeomorph.ext {α : Type u_1} {β : Type u_2} {h h' : α ≃ₜ β} (H : (x : α), h x = h' x) :
h = h'
@[simp]
theorem homeomorph.symm_symm {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
h.symm.symm = h
@[protected]
def homeomorph.refl (α : Type u_1)  :
α ≃ₜ α

Identity map as a homeomorphism.

Equations
@[simp]
theorem homeomorph.refl_apply (α : Type u_1)  :
@[protected]
def homeomorph.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) :
α ≃ₜ γ

Composition of two homeomorphisms.

Equations
@[simp]
theorem homeomorph.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) (a : α) :
(h₁.trans h₂) a = h₂ (h₁ a)
@[simp]
theorem homeomorph.homeomorph_mk_coe_symm {α : Type u_1} {β : Type u_2} (a : α β) (b : . "continuity'") (c : . "continuity'") :
@[simp]
theorem homeomorph.refl_symm {α : Type u_1}  :
@[protected, continuity]
theorem homeomorph.continuous {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected, continuity]
theorem homeomorph.continuous_symm {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.apply_symm_apply {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (x : β) :
h ((h.symm) x) = x
@[simp]
theorem homeomorph.symm_apply_apply {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (x : α) :
(h.symm) (h x) = x
@[simp]
theorem homeomorph.self_trans_symm {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
h.trans h.symm =
@[simp]
theorem homeomorph.symm_trans_self {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
h.symm.trans h =
@[protected]
theorem homeomorph.bijective {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.injective {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.surjective {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
def homeomorph.change_inv {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) (g : β α) (hg : f) :
α ≃ₜ β

Change the homeomorphism `f` to make the inverse function definitionally equal to `g`.

Equations
@[simp]
theorem homeomorph.symm_comp_self {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.self_comp_symm {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.range_coe {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
theorem homeomorph.image_symm {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
theorem homeomorph.preimage_symm {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
=
@[simp]
theorem homeomorph.image_preimage {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set β) :
h '' (h ⁻¹' s) = s
@[simp]
theorem homeomorph.preimage_image {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set α) :
h ⁻¹' (h '' s) = s
@[protected]
theorem homeomorph.inducing {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
theorem homeomorph.induced_eq {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
_inst_2 = _inst_1
@[protected]
theorem homeomorph.quotient_map {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
theorem homeomorph.coinduced_eq {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
_inst_1 = _inst_2
@[protected]
theorem homeomorph.embedding {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
noncomputable def homeomorph.of_embedding {α : Type u_1} {β : Type u_2} (f : α β) (hf : embedding f) :

Homeomorphism given an embedding.

Equations
@[protected]
theorem homeomorph.second_countable_topology {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
theorem homeomorph.is_compact_image {α : Type u_1} {β : Type u_2} {s : set α} (h : α ≃ₜ β) :
theorem homeomorph.is_compact_preimage {α : Type u_1} {β : Type u_2} {s : set β} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.comap_cocompact {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.map_cocompact {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.compact_space {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.t0_space {α : Type u_1} {β : Type u_2} [t0_space α] (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.t1_space {α : Type u_1} {β : Type u_2} [t1_space α] (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.t2_space {α : Type u_1} {β : Type u_2} [t2_space α] (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.t3_space {α : Type u_1} {β : Type u_2} [t3_space α] (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.dense_embedding {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.is_open_preimage {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) {s : set β} :
@[simp]
theorem homeomorph.is_open_image {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) {s : set α} :
@[protected]
theorem homeomorph.is_open_map {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[simp]
theorem homeomorph.is_closed_preimage {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) {s : set β} :
@[simp]
theorem homeomorph.is_closed_image {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) {s : set α} :
@[protected]
theorem homeomorph.is_closed_map {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.open_embedding {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.closed_embedding {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) :
@[protected]
theorem homeomorph.normal_space {α : Type u_1} {β : Type u_2} [normal_space α] (h : α ≃ₜ β) :
theorem homeomorph.preimage_closure {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set β) :
theorem homeomorph.image_closure {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set α) :
theorem homeomorph.preimage_interior {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set β) :
theorem homeomorph.image_interior {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set α) :
theorem homeomorph.preimage_frontier {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set β) :
theorem homeomorph.image_frontier {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (s : set α) :
theorem has_compact_support.comp_homeomorph {α : Type u_1} {β : Type u_2} {M : Type u_3} [has_zero M] {f : β M} (hf : has_compact_support f) (φ : α ≃ₜ β) :
theorem has_compact_mul_support.comp_homeomorph {α : Type u_1} {β : Type u_2} {M : Type u_3} [has_one M] {f : β M} (hf : has_compact_mul_support f) (φ : α ≃ₜ β) :
@[simp]
theorem homeomorph.map_nhds_eq {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (x : α) :
(nhds x) = nhds (h x)
theorem homeomorph.symm_map_nhds_eq {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (x : α) :
theorem homeomorph.nhds_eq_comap {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (x : α) :
nhds x = (nhds (h x))
@[simp]
theorem homeomorph.comap_nhds_eq {α : Type u_1} {β : Type u_2} (h : α ≃ₜ β) (y : β) :
(nhds y) = nhds ((h.symm) y)
def homeomorph.homeomorph_of_continuous_open {α : Type u_1} {β : Type u_2} (e : α β) (h₁ : continuous e) (h₂ : is_open_map e) :
α ≃ₜ β

If an bijective map `e : α ≃ β` is continuous and open, then it is a homeomorphism.

Equations
@[simp]
theorem homeomorph.comp_continuous_on_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) (f : γ α) (s : set γ) :
@[simp]
theorem homeomorph.comp_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) {f : γ α} :
@[simp]
theorem homeomorph.comp_continuous_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) {f : β γ} :
theorem homeomorph.comp_continuous_at_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) (f : γ α) (x : γ) :
theorem homeomorph.comp_continuous_at_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) (f : β γ) (x : α) :
theorem homeomorph.comp_continuous_within_at_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) (f : γ α) (s : set γ) (x : γ) :
@[simp]
theorem homeomorph.comp_is_open_map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) {f : γ α} :
@[simp]
theorem homeomorph.comp_is_open_map_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α ≃ₜ β) {f : β γ} :
def homeomorph.set_congr {α : Type u_1} {s t : set α} (h : s = t) :

If two sets are equal, then they are homeomorphic.

Equations
def homeomorph.sum_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :
α γ ≃ₜ β δ

Sum of two homeomorphisms.

Equations
def homeomorph.prod_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :
α × γ ≃ₜ β × δ

Product of two homeomorphisms.

Equations
@[simp]
theorem homeomorph.prod_congr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (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} (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :
(h₁.prod_congr h₂) = h₂
def homeomorph.prod_comm (α : Type u_1) (β : Type u_2)  :
α × β ≃ₜ β × α

`α × β` is homeomorphic to `β × α`.

Equations
@[simp]
theorem homeomorph.prod_comm_symm (α : Type u_1) (β : Type u_2)  :
@[simp]
theorem homeomorph.coe_prod_comm (α : Type u_1) (β : Type u_2)  :
def homeomorph.prod_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3)  :
× β) × γ ≃ₜ α × β × γ

`(α × β) × γ` is homeomorphic to `α × (β × γ)`.

Equations
@[simp]
theorem homeomorph.prod_punit_apply (α : Type u_1)  :
def homeomorph.prod_punit (α : Type u_1)  :
≃ₜ α

`α × {*}` is homeomorphic to `α`.

Equations
def homeomorph.punit_prod (α : Type u_1)  :
≃ₜ α

`{*} × α` is homeomorphic to `α`.

Equations
@[simp]
theorem homeomorph.coe_punit_prod (α : Type u_1)  :
@[simp]
theorem homeomorph.homeomorph_of_unique_apply (α : Type u_1) (β : Type u_2) [unique α] [unique β] (ᾰ : α) :
= .to_fun
def homeomorph.homeomorph_of_unique (α : Type u_1) (β : Type u_2) [unique α] [unique β] :
α ≃ₜ β

If both `α` and `β` have a unique element, then `α ≃ₜ β`.

Equations
@[simp]
theorem homeomorph.homeomorph_of_unique_symm_apply (α : Type u_1) (β : Type u_2) [unique α] [unique β] (ᾰ : β) :
.symm) = .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) :
= 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 : ι) :
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
@[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 (λ (i : ι), (F i).symm)
def homeomorph.ulift {α : Type u}  :
≃ₜ α

`ulift α` is homeomorphic to `α`.

Equations
def homeomorph.sum_prod_distrib {α : Type u_1} {β : Type u_2} {γ : Type u_3}  :
β) × γ ≃ₜ α × γ β × γ

`(α ⊕ β) × γ` is homeomorphic to `α × γ ⊕ β × γ`.

Equations
def homeomorph.prod_sum_distrib {α : Type u_1} {β : Type u_2} {γ : Type u_3}  :
α × γ) ≃ₜ α × β α × γ

`α × (β ⊕ γ)` is homeomorphic to `α × β ⊕ α × γ`.

Equations
def homeomorph.sigma_prod_distrib {β : Type u_2} {ι : Type u_5} {σ : ι Type u_6} [Π (i : ι), topological_space (σ i)] :
(Σ (i : ι), σ i) × β ≃ₜ Σ (i : ι), σ i × β

`(Σ i, σ i) × β` is homeomorphic to `Σ i, (σ i × β)`.

Equations
def homeomorph.fun_unique (ι : Type u_1) (α : Type u_2) [unique ι]  :
α) ≃ₜ α

If `ι` has a unique element, then `ι → α` is homeomorphic to `α`.

Equations
@[simp]
theorem homeomorph.fun_unique_apply (ι : Type u_1) (α : Type u_2) [unique ι]  :
@[simp]
theorem homeomorph.fun_unique_symm_apply (ι : Type u_1) (α : Type u_2) [unique ι]  :
α).symm) = λ (x : α) (b : ι), x
@[simp]
theorem homeomorph.pi_fin_two_symm_apply (α : fin 2 Type u) [Π (i : fin 2), topological_space (α i)] :
.symm) = λ (p : α 0 × α 1),
def homeomorph.pi_fin_two (α : fin 2 Type u) [Π (i : fin 2), topological_space (α i)] :
(Π (i : fin 2), α i) ≃ₜ α 0 × α 1

Homeomorphism between dependent functions `Π i : fin 2, α i` and `α 0 × α 1`.

Equations
@[simp]
theorem homeomorph.pi_fin_two_apply (α : fin 2 Type u) [Π (i : fin 2), topological_space (α i)] :
= λ (f : Π (i : fin 2), α i), (f 0, f 1)
@[simp]
theorem homeomorph.fin_two_arrow_apply {α : Type u_1}  :
homeomorph.fin_two_arrow = λ (f : fin 2 α), (f 0, f 1)
@[simp]
theorem homeomorph.fin_two_arrow_symm_apply {α : Type u_1}  :
(homeomorph.fin_two_arrow.symm) = λ (x : α × α), ![x.fst, x.snd]
def homeomorph.fin_two_arrow {α : Type u_1}  :
(fin 2 α) ≃ₜ α × α

Homeomorphism between `α² = fin 2 → α` and `α × α`.

Equations
@[simp]
theorem homeomorph.image_symm_apply_coe {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) (s : set α) (y : ((e.to_equiv) '' s)) :
(((e.image s).symm) y) = (e.symm) y
@[simp]
theorem homeomorph.image_apply_coe {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) (s : set α) (x : s) :
((e.image s) x) = e x
def homeomorph.image {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) (s : set α) :

A subset of a topological space is homeomorphic to its image under a homeomorphism.

Equations
@[simp]
theorem homeomorph.set.univ_apply (α : Type u_1)  :
def homeomorph.set.univ (α : Type u_1)  :

`set.univ α` is homeomorphic to `α`.

Equations
@[simp]
theorem homeomorph.set.univ_symm_apply_coe (α : Type u_1) (a : α) :
(.symm) a) = a
@[simp]
theorem homeomorph.set.prod_apply {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) (x : {c // s c.fst t c.snd}) :
t) x = (x.fst, _⟩, x.snd, _⟩)
@[simp]
theorem homeomorph.set.prod_symm_apply_coe {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) (x : {a // s a} × {b // t b}) :
( t).symm) x) = ((x.fst), (x.snd))
def homeomorph.set.prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :

`s ×ˢ t` is homeomorphic to `s × t`.

Equations
@[simp]
theorem homeomorph.pi_equiv_pi_subtype_prod_apply {ι : Type u_5} (p : ι Prop) (β : ι Type u_1) [Π (i : ι), topological_space (β i)] (f : Π (i : ι), β i) :
= (λ (x : subtype p), f x, λ (x : {x // ¬p x}), f x)
@[simp]
theorem homeomorph.pi_equiv_pi_subtype_prod_symm_apply {ι : Type u_5} (p : ι Prop) (β : ι Type u_1) [Π (i : ι), topological_space (β i)] (f : (Π (i : {x // p x}), β i) × Π (i : {x // ¬p x}), β i) (x : ι) :
f x = dite (p x) (λ (h : p x), f.fst x, h⟩) (λ (h : ¬p x), f.snd x, h⟩)
def homeomorph.pi_equiv_pi_subtype_prod {ι : Type u_5} (p : ι Prop) (β : ι Type u_1) [Π (i : ι), topological_space (β i)]  :
(Π (i : ι), β i) ≃ₜ (Π (i : {x // p x}), β i) × Π (i : {x // ¬p x}), β i

The topological space `Π i, β i` can be split as a product by separating the indices in ι depending on whether they satisfy a predicate p or not.

Equations
@[simp]
theorem homeomorph.pi_split_at_apply {ι : Type u_5} [decidable_eq ι] (i : ι) (β : ι Type u_1) [Π (j : ι), topological_space (β j)] (f : Π (j : ι), β j) :
f = (f i, λ (j : {j // ¬j = i}), f j)
def homeomorph.pi_split_at {ι : Type u_5} [decidable_eq ι] (i : ι) (β : ι Type u_1) [Π (j : ι), topological_space (β j)] :
(Π (j : ι), β j) ≃ₜ β i × Π (j : {j // j i}), β j

A product of topological spaces can be split as the binary product of one of the spaces and the product of all the remaining spaces.

Equations
@[simp]
theorem homeomorph.pi_split_at_symm_apply {ι : Type u_5} [decidable_eq ι] (i : ι) (β : ι Type u_1) [Π (j : ι), topological_space (β j)] (f : β i × Π (j : {j // j i}), β j) (j : ι) :
β).symm) f j = dite (j = i) (λ (h : j = i), eq.rec f.fst _) (λ (h : ¬j = i), f.snd j, h⟩)
@[simp]
theorem homeomorph.fun_split_at_apply (β : Type u_2) {ι : Type u_5} [decidable_eq ι] (i : ι) (f : Π (j : ι), (λ (ᾰ : ι), β) j) :
f = (f i, λ (j : {j // ¬j = i}), f j)
@[simp]
theorem homeomorph.fun_split_at_symm_apply (β : Type u_2) {ι : Type u_5} [decidable_eq ι] (i : ι) (f : (λ (ᾰ : ι), β) i × Π (j : {j // j i}), (λ (ᾰ : ι), β) j) (j : ι) :
i).symm) f j = dite (j = i) (λ (h : j = i), f.fst) (λ (h : ¬j = i), f.snd j, h⟩)
def homeomorph.fun_split_at (β : Type u_2) {ι : Type u_5} [decidable_eq ι] (i : ι) :
β) ≃ₜ β × ({j // j i} β)

A product of copies of a topological space can be split as the binary product of one copy and the product of all the remaining copies.

Equations
• = (λ (ᾰ : ι), β)
@[simp]
theorem equiv.to_homeomorph_of_inducing_symm_apply {α : Type u_1} {β : Type u_2} (f : α β) (hf : inducing f) (ᾰ : β) :
@[simp]
theorem equiv.to_homeomorph_of_inducing_apply {α : Type u_1} {β : Type u_2} (f : α β) (hf : inducing f) (ᾰ : α) :
= f.to_fun
def equiv.to_homeomorph_of_inducing {α : Type u_1} {β : Type u_2} (f : α β) (hf : inducing f) :
α ≃ₜ β

An inducing equiv between topological spaces is a homeomorphism.

Equations
theorem continuous.continuous_symm_of_equiv_compact_to_t2 {α : Type u_1} {β : Type u_2} [t2_space β] {f : α β} (hf : continuous f) :
def continuous.homeo_of_equiv_compact_to_t2 {α : Type u_1} {β : Type u_2} [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
@[simp]
theorem continuous.homeo_of_equiv_compact_to_t2_apply {α : Type u_1} {β : Type u_2} [t2_space β] {f : α β} (hf : continuous f) (ᾰ : α) :
= f.to_fun
@[simp]
theorem continuous.homeo_of_equiv_compact_to_t2_symm_apply {α : Type u_1} {β : Type u_2} [t2_space β] {f : α β} (hf : continuous f) (ᾰ : β) :
= f.inv_fun