mathlib documentation

topology.homeomorph

@[nolint]
structure homeomorph (α : Type u_5) (β : Type u_6) [topological_space α] [topological_space β] :
Type (max u_5 u_6)

Homeomorphism between α and β, also called topological isomorphism

@[instance]
def homeomorph.has_coe_to_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

Equations
@[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'") :

theorem homeomorph.coe_eq_to_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (a : α) :
h a = (h.to_equiv) a

@[ext]
theorem homeomorph.ext {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {h h' : α ≃ₜ β} (H : ∀ (x : α), h x = h' x) :
h = h'

def homeomorph.refl (α : Type u_1) [topological_space α] :
α ≃ₜ α

Identity map as a homeomorphism.

Equations
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
def homeomorph.symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) :
β ≃ₜ α

Inverse of a homeomorphism.

Equations
@[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'") :

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 : β) :
h ((h.symm) x) = x

@[simp]
theorem homeomorph.symm_apply_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (x : α) :
(h.symm) (h x) = 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
@[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 β) :
h '' (h ⁻¹' s) = s

@[simp]
theorem homeomorph.preimage_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (s : set α) :
h ⁻¹' (h '' s) = s

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 : α ≃ₜ β) :

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 : α ≃ₜ β) :

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 : α ≃ₜ β) :

theorem homeomorph.compact_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set β} (h : α ≃ₜ β) :

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
@[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 γ) :

@[simp]
theorem homeomorph.comp_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (h : α ≃ₜ β) {f : γ → α} :

@[simp]
theorem homeomorph.comp_continuous_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (h : α ≃ₜ β) {f : β → γ} :

def homeomorph.set_congr {α : Type u_1} [topological_space α] {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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) :
α γ ≃ₜ β δ

Sum of two homeomorphisms.

Equations
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
def homeomorph.prod_comm (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] :
α × β ≃ₜ β × α

α × β is homeomorphic to β × α.

Equations
def homeomorph.prod_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) [topological_space α] [topological_space β] [topological_space γ] :
× β) × γ ≃ₜ α × β × γ

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

Equations
def homeomorph.ulift {α : Type u} [topological_space α] :

ulift α is homeomorphic to α.

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

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

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

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

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

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

Equations