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

Instances for homeomorph

source

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

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

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

@[simp]

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

⇑(h.to_equiv) = ⇑h

source

@[simp]

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

⇑(h.to_equiv.symm) = ⇑(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

@[simp]

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

h.symm.symm = h

source

@[protected]

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

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

source

@[simp]

theorem homeomorph.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) (a : α) :

⇑(h₁.trans h₂) a = ⇑h₂ (⇑h₁ a)

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

@[protected, continuity]

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

continuous ⇑h

source

@[protected, continuity]

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

@[simp]

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

h.trans h.symm = homeomorph.refl α

source

@[simp]

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

h.symm.trans h = homeomorph.refl β

source

@[protected]

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

function.bijective ⇑h

source

@[protected]

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

function.injective ⇑h

source

@[protected]

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

@[protected]

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

@[protected]

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

@[protected]

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

embedding ⇑h

source

noncomputable 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 := equiv.of_injective f _, continuous_to_fun := _, continuous_inv_fun := _}

source

@[protected]

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.is_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.is_compact_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set β} (h : α ≃ₜ β) :

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

source

@[simp]

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

filter.comap ⇑h (filter.cocompact β) = filter.cocompact α

source

@[simp]

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

filter.map ⇑h (filter.cocompact α) = filter.cocompact β

source

@[protected]

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

compact_space β

source

@[protected]

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

t0_space β

source

@[protected]

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

t1_space β

source

@[protected]

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

t2_space β

source

@[protected]

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

t3_space β

source

@[protected]

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

@[protected]

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

is_open_map ⇑h

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

@[protected]

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

is_closed_map ⇑h

source

@[protected]

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

open_embedding ⇑h

source

@[protected]

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

closed_embedding ⇑h

source

@[protected]

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

normal_space β

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.preimage_interior {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (h : α ≃ₜ β) (s : set β) :

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

source

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

⇑h '' interior s = interior (⇑h '' s)

source

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

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

source

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

⇑h '' frontier s = frontier (⇑h '' s)

source

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 ∘ ⇑φ)

source

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 ∘ ⇑φ)

source

@[simp]

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

filter.map ⇑h (nhds x) = nhds (⇑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) (nhds (⇑h x)) = nhds x

source

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

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

source

@[simp]

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

filter.comap ⇑h (nhds y) = nhds (⇑(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

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

source

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)

source

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

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

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

source

@[simp]

theorem homeomorph.prod_comm_symm (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] :

(homeomorph.prod_comm α β).symm = homeomorph.prod_comm β α

source

@[simp]

theorem homeomorph.coe_prod_comm (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] :

⇑(homeomorph.prod_comm α β) = prod.swap

source

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

source

@[simp]

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

⇑(homeomorph.prod_punit α) = prod.fst

source

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

α × punit ≃ₜ α

α × {*} is homeomorphic to α.

Equations

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

source

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

punit × α ≃ₜ α

{*} × α is homeomorphic to α.

Equations

homeomorph.punit_prod α = (homeomorph.prod_comm punit α).trans (homeomorph.prod_punit α)

source

@[simp]

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

⇑(homeomorph.punit_prod α) = prod.snd

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

ulift α ≃ₜ α

ulift α is homeomorphic to α.

Equations

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

source

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

source

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 γ α)))

source

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

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

source

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

source

@[simp]

theorem homeomorph.fun_unique_apply (ι : Type u_1) (α : Type u_2) [unique ι] [topological_space α] :

⇑(homeomorph.fun_unique ι α) = function.eval inhabited.default

source

@[simp]

theorem homeomorph.fun_unique_symm_apply (ι : Type u_1) (α : Type u_2) [unique ι] [topological_space α] :

⇑((homeomorph.fun_unique ι α).symm) = λ (x : α) (b : ι), x

source

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

source

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

homeomorph.pi_fin_two α = {to_equiv := pi_fin_two_equiv α, continuous_to_fun := _, continuous_inv_fun := _}

source

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

source

@[simp]

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

⇑homeomorph.fin_two_arrow = λ (f : fin 2 → α), (f 0, f 1)

source

@[simp]

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

⇑(homeomorph.fin_two_arrow.symm) = λ (x : α × α), ![x.fst, x.snd]

source

def homeomorph.fin_two_arrow {α : Type u_1} [topological_space α] :

(fin 2 → α) ≃ₜ α × α

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

Equations

homeomorph.fin_two_arrow = {to_equiv := fin_two_arrow_equiv α, continuous_to_fun := _, continuous_inv_fun := _}

source

@[simp]

theorem homeomorph.image_symm_apply_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) (s : set α) (y : ↥(⇑(e.to_equiv) '' s)) :

↑(⇑((e.image s).symm) y) = ⇑(e.symm) ↑y

source

@[simp]

theorem homeomorph.image_apply_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) (s : set α) (x : ↥s) :

↑(⇑(e.image s) x) = ⇑e ↑x

source

def homeomorph.image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) (s : set α) :

↥s ≃ₜ ↥(⇑e '' s)

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

source

@[simp]

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

⇑(homeomorph.set.univ α) = coe

source

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

↥set.univ ≃ₜ α

set.univ α is homeomorphic to α.

Equations

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

source

@[simp]

theorem homeomorph.set.univ_symm_apply_coe (α : Type u_1) [topological_space α] (a : α) :

↑(⇑((homeomorph.set.univ α).symm) a) = a

source

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

⇑(homeomorph.set.prod s t) x = (⟨↑x.fst, _⟩, ⟨↑x.snd, _⟩)

source

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

↑(⇑((homeomorph.set.prod s t).symm) x) = (↑(x.fst), ↑(x.snd))

source

def homeomorph.set.prod {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) (t : set β) :

↥(s ×ˢ t) ≃ₜ ↥s × ↥t

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

source

@[simp]

theorem homeomorph.pi_equiv_pi_subtype_prod_apply {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_1) [Π (i : ι), topological_space (β i)] [decidable_pred p] (f : Π (i : ι), β i) :

⇑(homeomorph.pi_equiv_pi_subtype_prod p β) f = (λ (x : subtype p), f ↑x, λ (x : {x // ¬p x}), f ↑x)

source

@[simp]

theorem homeomorph.pi_equiv_pi_subtype_prod_symm_apply {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_1) [Π (i : ι), topological_space (β i)] [decidable_pred p] (f : (Π (i : {x // p x}), β ↑i) × Π (i : {x // ¬p x}), β ↑i) (x : ι) :

⇑((homeomorph.pi_equiv_pi_subtype_prod p β).symm) f x = dite (p x) (λ (h : p x), f.fst ⟨x, h⟩) (λ (h : ¬p x), f.snd ⟨x, h⟩)

source

def homeomorph.pi_equiv_pi_subtype_prod {ι : Type u_5} (p : ι → Prop) (β : ι → Type u_1) [Π (i : ι), topological_space (β i)] [decidable_pred p] :

(Π (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

homeomorph.pi_equiv_pi_subtype_prod p β = {to_equiv := equiv.pi_equiv_pi_subtype_prod p β (λ (a : ι), _inst_6 a), continuous_to_fun := _, continuous_inv_fun := _}

source

@[simp]

theorem homeomorph.pi_split_at_apply {ι : Type u_5} [decidable_eq ι] (i : ι) (β : ι → Type u_1) [Π (j : ι), topological_space (β j)] (f : Π (j : ι), β j) :

⇑(homeomorph.pi_split_at i β) f = (f i, λ (j : {j // ¬j = i}), f ↑j)

source

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

homeomorph.pi_split_at i β = {to_equiv := equiv.pi_split_at i β, continuous_to_fun := _, continuous_inv_fun := _}

source

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

⇑((homeomorph.pi_split_at i β).symm) f j = dite (j = i) (λ (h : j = i), eq.rec f.fst _) (λ (h : ¬j = i), f.snd ⟨j, h⟩)

source

@[simp]

theorem homeomorph.fun_split_at_apply (β : Type u_2) [topological_space β] {ι : Type u_5} [decidable_eq ι] (i : ι) (f : Π (j : ι), (λ (ᾰ : ι), β) j) :

⇑(homeomorph.fun_split_at β i) f = (f i, λ (j : {j // ¬j = i}), f ↑j)

source

@[simp]

theorem homeomorph.fun_split_at_symm_apply (β : Type u_2) [topological_space β] {ι : Type u_5} [decidable_eq ι] (i : ι) (f : (λ (ᾰ : ι), β) i × Π (j : {j // j ≠ i}), (λ (ᾰ : ι), β) ↑j) (j : ι) :

⇑((homeomorph.fun_split_at β i).symm) f j = dite (j = i) (λ (h : j = i), f.fst) (λ (h : ¬j = i), f.snd ⟨j, h⟩)

source

def homeomorph.fun_split_at (β : Type u_2) [topological_space β] {ι : 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

homeomorph.fun_split_at β i = homeomorph.pi_split_at i (λ (ᾰ : ι), β)

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

mathlib3 documentation

Homeomorphisms #

Main definitions #

Main results #