topology.homeomorph - mathlib docs

source

@[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

source

@[instance]

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

has_coe_to_fun (α ≃ₜ β) (λ (_x : α ≃ₜ β), α → β)

Equations

homeomorph.has_coe_to_fun = {coe := λ (e : α ≃ₜ β), ⇑(e.to_equiv)}

source

@[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

source

@[simp]

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

⇑(h.to_equiv) = ⇑h

source

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 := _}

source

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

homeomorph.simps.apply h = ⇑h

source

def homeomorph.simps.symm_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) :

β → α

See Note [custom simps projection]

Equations

homeomorph.simps.symm_apply h = ⇑(h.symm)

source

theorem homeomorph.to_equiv_injective {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

function.injective homeomorph.to_equiv

source

@[ext]

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

h = h'

source

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

α ≃ₜ α

Identity map as a homeomorphism.

Equations

homeomorph.refl α = {to_equiv := equiv.refl α, continuous_to_fun := _, continuous_inv_fun := _}

source

@[simp]

theorem homeomorph.refl_apply (α : Type u_1) [topological_space α] :

⇑(homeomorph.refl α) = id

source

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 := _}

source

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

source

@[simp]

theorem homeomorph.refl_symm {α : Type u_1} [topological_space α] :

(homeomorph.refl α).symm = homeomorph.refl α

source

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

continuous ⇑h

source

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

continuous ⇑(h.symm)

source

@[simp]

theorem homeomorph.apply_symm_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (x : β) :

⇑h (⇑(h.symm) x) = x

source

@[simp]

theorem homeomorph.symm_apply_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (x : α) :

⇑(h.symm) (⇑h x) = x

source

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

function.bijective ⇑h

source

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

function.injective ⇑h

source

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

function.surjective ⇑h

source

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 := _}

source

@[simp]

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

⇑(h.symm) ∘ ⇑h = id

source

@[simp]

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

⇑h ∘ ⇑(h.symm) = id

source

@[simp]

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

set.range ⇑h = set.univ

source

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

set.image ⇑(h.symm) = set.preimage ⇑h

source

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

set.preimage ⇑(h.symm) = set.image ⇑h

source

@[simp]

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

⇑h '' (⇑h ⁻¹' s) = s

source

@[simp]

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

⇑h ⁻¹' (⇑h '' s) = s

source

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

inducing ⇑h

source

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

topological_space.induced ⇑h _inst_2 = _inst_1

source

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

quotient_map ⇑h

source

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

topological_space.coinduced ⇑h _inst_1 = _inst_2

source

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

embedding ⇑h

source

def homeomorph.of_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : embedding f) :

α ≃ₜ ↥(set.range 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 := _}

source

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

topological_space.second_countable_topology α

source

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

is_compact (⇑h '' s) ↔ is_compact s

source

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

is_compact (⇑h ⁻¹' s) ↔ is_compact s

source

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

compact_space β

source

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

t2_space β

source

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

dense_embedding ⇑h

source

@[simp]

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

is_open (⇑h ⁻¹' s) ↔ is_open s

source

@[simp]

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

is_open (⇑h '' s) ↔ is_open s

source

@[simp]

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

is_closed (⇑h ⁻¹' s) ↔ is_closed s

source

@[simp]

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

is_closed (⇑h '' s) ↔ is_closed s

source

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

⇑h ⁻¹' closure s = closure (⇑h ⁻¹' s)

source

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

⇑h '' closure s = closure (⇑h '' s)

source

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

is_open_map ⇑h

source

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

is_closed_map ⇑h

source

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

closed_embedding ⇑h

source

@[simp]

theorem homeomorph.map_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (x : α) :

filter.map ⇑h (𝓝 x) = 𝓝 (⇑h x)

source

theorem homeomorph.symm_map_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (x : α) :

filter.map ⇑(h.symm) (𝓝 (⇑h x)) = 𝓝 x

source

theorem homeomorph.nhds_eq_comap {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (x : α) :

𝓝 x = filter.comap ⇑h (𝓝 (⇑h x))

source

@[simp]

theorem homeomorph.comap_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (y : β) :

filter.comap ⇑h (𝓝 y) = 𝓝 (⇑(h.symm) y)

source

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 := _}

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

def homeomorph.set_congr {α : Type u_1} [topological_space α] {s t : set α} (h : s = t) :

↥s ≃ₜ ↥t

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 := _}

source

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 := _}

source

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 := _}

source

@[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

source

@[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₂ : γ ≃ₜ δ) :

⇑(h₁.prod_congr h₂) = prod.map ⇑h₁ ⇑h₂

source