Homeomorphisms

This file defines homeomorphisms between two topological spaces. They are bijections with both directions continuous. We denote homeomorphisms with the notation ≃ₜ.

Main definitions and results

• Homeomorph X Y: The type of homeomorphisms from X to Y. This type can be denoted using the following notation: X ≃ₜ Y.

• HomeomorphClass: HomeomorphClass F A B states that F is a type of homeomorphisms.

• Homeomorph.symm: the inverse of a homeomorphism

• Homeomorph.trans: composing two homeomorphisms

• Homeomorphisms are open and closed embeddings, inducing, quotient maps etc.

• Homeomorph.homeomorphOfContinuousOpen: A continuous bijection that is an open map is a homeomorphism.

• Homeomorph.homeomorphOfUnique: if both X and Y have a unique element, then X ≃ₜ Y.

• Equiv.toHomeomorph: an equivalence between topological spaces respecting openness is a homeomorphism.

• IsHomeomorph: the predicate that a function is a homeomorphism

structure Homeomorph (X : Type u_5) (Y : Type u_6) [TopologicalSpace X] [TopologicalSpace Y] extends X ≃ Y : Type (max u_5 u_6)

Homeomorphism between X and Y, also called topological isomorphism

• toFun : X → Y
• invFun : Y → X
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• continuous_toFun : Continuous self.toFun

  The forward map of a homeomorphism is a continuous function.

• continuous_invFun : Continuous self.invFun

  The inverse map of a homeomorphism is a continuous function.

def «term_≃ₜ_» : Lean.TrailingParserDescr

Homeomorphism between X and Y, also called topological isomorphism

Equations

• «term_≃ₜ_» = Lean.ParserDescr.trailingNode `«term_≃ₜ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₜ ") (Lean.ParserDescr.cat `term 26))

theorem Homeomorph.toEquiv_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Function.Injective toEquiv

instance Homeomorph.instEquivLike {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : EquivLike (X ≃ₜ Y) X Y

Equations

• Homeomorph.instEquivLike = { coe := fun (h : X ≃ₜ Y) => ⇑h.toEquiv, inv := fun (h : X ≃ₜ Y) => ⇑h.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

@[simp]

theorem Homeomorph.homeomorph_mk_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (a : X ≃ Y) (b : Continuous a.toFun) (c : Continuous a.invFun) : ⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c } = ⇑a

def Homeomorph.empty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty X] [IsEmpty Y] : X ≃ₜ Y

The unique homeomorphism between two empty types.

Equations

• Homeomorph.empty = { toEquiv := Equiv.equivOfIsEmpty X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Y ≃ₜ X

Inverse of a homeomorphism.

Equations

• h.symm = { toEquiv := h.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.symm_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : h.symm.symm = h

theorem Homeomorph.symm_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Function.Bijective Homeomorph.symm

def Homeomorph.Simps.symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Y → X

See Note [custom simps projection]

Equations

• Homeomorph.Simps.symm_apply h = ⇑h.symm

@[simp]

theorem Homeomorph.coe_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h.toEquiv = ⇑h

@[simp]

theorem Homeomorph.coe_symm_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h.symm = ⇑h.symm

theorem Homeomorph.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {h h' : X ≃ₜ Y} (H : ∀ (x : X), h x = h' x) : h = h'

theorem Homeomorph.ext_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {h h' : X ≃ₜ Y} : h = h' ↔ ∀ (x : X), h x = h' x

def Homeomorph.refl (X : Type u_7) [TopologicalSpace X] : X ≃ₜ X

Identity map as a homeomorphism.

Equations

• Homeomorph.refl X = { toEquiv := Equiv.refl X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.refl_apply (X : Type u_7) [TopologicalSpace X] : ⇑(Homeomorph.refl X) = id

def Homeomorph.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z

Composition of two homeomorphisms.

Equations

• h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) (x : X) : (h₁.trans h₂) x = h₂ (h₁ x)

@[simp]

theorem Homeomorph.symm_trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X ≃ₜ Y) (g : Y ≃ₜ Z) (z : Z) : (f.trans g).symm z = f.symm (g.symm z)

@[simp]

theorem Homeomorph.homeomorph_mk_coe_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (a : X ≃ Y) (b : Continuous a.toFun) (c : Continuous a.invFun) : ⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c }.symm = ⇑a.symm

@[simp]

theorem Homeomorph.refl_symm {X : Type u_1} [TopologicalSpace X] : (Homeomorph.refl X).symm = Homeomorph.refl X

theorem Homeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Continuous ⇑h

theorem Homeomorph.continuous_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Continuous ⇑h.symm

@[simp]

theorem Homeomorph.apply_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y) : h (h.symm y) = y

@[simp]

theorem Homeomorph.symm_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : h.symm (h x) = x

@[simp]

theorem Homeomorph.self_trans_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : h.trans h.symm = Homeomorph.refl X

@[simp]

theorem Homeomorph.symm_trans_self {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : h.symm.trans h = Homeomorph.refl Y

theorem Homeomorph.bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Function.Bijective ⇑h

theorem Homeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Function.Injective ⇑h

theorem Homeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Function.Surjective ⇑h

def Homeomorph.changeInv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (g : Y → X) (hg : Function.RightInverse g ⇑f) : X ≃ₜ Y

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

Equations

• f.changeInv g hg = { toFun := ⇑f, invFun := g, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.symm_comp_self {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h.symm ∘ ⇑h = id

@[simp]

theorem Homeomorph.self_comp_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ⇑h ∘ ⇑h.symm = id

theorem Homeomorph.range_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Set.range ⇑h = Set.univ

theorem Homeomorph.image_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Set.image ⇑h.symm = Set.preimage ⇑h

theorem Homeomorph.preimage_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Set.preimage ⇑h.symm = Set.image ⇑h

@[simp]

theorem Homeomorph.image_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h '' (⇑h ⁻¹' s) = s

@[simp]

theorem Homeomorph.preimage_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h ⁻¹' (⇑h '' s) = s

theorem Homeomorph.image_eq_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' s = ⇑h.symm ⁻¹' s

theorem Homeomorph.image_compl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' sᶜ = (⇑h '' s)ᶜ

theorem Homeomorph.isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsInducing ⇑h

@[deprecated Homeomorph.isInducing (since := "2024-10-28")]

theorem Homeomorph.inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsInducing ⇑h

Alias of Homeomorph.isInducing.

theorem Homeomorph.induced_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : TopologicalSpace.induced (⇑h) inst✝ = inst✝¹

theorem Homeomorph.isQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsQuotientMap ⇑h

@[deprecated Homeomorph.isQuotientMap (since := "2024-10-22")]

theorem Homeomorph.quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsQuotientMap ⇑h

Alias of Homeomorph.isQuotientMap.

theorem Homeomorph.coinduced_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : TopologicalSpace.coinduced (⇑h) inst✝ = inst✝¹

theorem Homeomorph.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsEmbedding ⇑h

@[deprecated Homeomorph.isEmbedding (since := "2024-10-26")]

theorem Homeomorph.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsEmbedding ⇑h

Alias of Homeomorph.isEmbedding.

theorem Homeomorph.discreteTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] (h : X ≃ₜ Y) : DiscreteTopology Y

theorem Homeomorph.discreteTopology_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : DiscreteTopology X ↔ DiscreteTopology Y

@[simp]

theorem Homeomorph.isOpen_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y} : IsOpen (⇑h ⁻¹' s) ↔ IsOpen s

@[simp]

theorem Homeomorph.isOpen_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X} : IsOpen (⇑h '' s) ↔ IsOpen s

theorem Homeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsOpenMap ⇑h

theorem Homeomorph.isOpenQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsOpenQuotientMap ⇑h

@[simp]

theorem Homeomorph.isClosed_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y} : IsClosed (⇑h ⁻¹' s) ↔ IsClosed s

@[simp]

theorem Homeomorph.isClosed_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X} : IsClosed (⇑h '' s) ↔ IsClosed s

theorem Homeomorph.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsClosedMap ⇑h

theorem Homeomorph.isOpenEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsOpenEmbedding ⇑h

theorem Homeomorph.isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsClosedEmbedding ⇑h

theorem Homeomorph.preimage_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h ⁻¹' closure s = closure (⇑h ⁻¹' s)

theorem Homeomorph.image_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' closure s = closure (⇑h '' s)

theorem Homeomorph.preimage_interior {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h ⁻¹' interior s = interior (⇑h ⁻¹' s)

theorem Homeomorph.image_interior {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' interior s = interior (⇑h '' s)

theorem Homeomorph.preimage_frontier {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h ⁻¹' frontier s = frontier (⇑h ⁻¹' s)

theorem Homeomorph.image_frontier {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' frontier s = frontier (⇑h '' s)

@[simp]

theorem Homeomorph.comp_continuous_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Z → X} : Continuous (⇑h ∘ f) ↔ Continuous f

@[simp]

theorem Homeomorph.comp_continuous_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z} : Continuous (f ∘ ⇑h) ↔ Continuous f

theorem Homeomorph.comp_continuousAt_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (z : Z) : ContinuousAt (⇑h ∘ f) z ↔ ContinuousAt f z

theorem Homeomorph.comp_continuousAt_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : Y → Z) (x : X) : ContinuousAt (f ∘ ⇑h) x ↔ ContinuousAt f (h x)

@[simp]

theorem Homeomorph.comp_isOpenMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Z → X} : IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f

@[simp]

theorem Homeomorph.comp_isOpenMap_iff' {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f

def Homeomorph.homeomorphOfUnique (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] : X ≃ₜ Y

If both X and Y have a unique element, then X ≃ₜ Y.

Equations

• Homeomorph.homeomorphOfUnique X Y = { toEquiv := Equiv.ofUnique X Y, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Homeomorph.homeomorphOfUnique_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] (a✝ : X) : (homeomorphOfUnique X Y) a✝ = default

@[simp]

theorem Homeomorph.homeomorphOfUnique_symm_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] (a✝ : Y) : (homeomorphOfUnique X Y).symm a✝ = default

@[simp]

theorem Homeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h) (nhds x) = nhds (h x)

theorem Homeomorph.symm_map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h.symm) (nhds (h x)) = nhds x

theorem Homeomorph.nhds_eq_comap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : nhds x = Filter.comap (⇑h) (nhds (h x))

@[simp]

theorem Homeomorph.comap_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y) : Filter.comap (⇑h) (nhds y) = nhds (h.symm y)

def Equiv.toHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : X ≃ₜ Y

An equivalence between topological spaces respecting openness is a homeomorphism.

Equations

• e.toHomeomorph he = { toEquiv := e, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Equiv.toHomeomorph_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toHomeomorph he).toEquiv = e

@[simp]

theorem Equiv.coe_toHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : ⇑(e.toHomeomorph he) = ⇑e

theorem Equiv.toHomeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (x : X) : (e.toHomeomorph he) x = e x

@[simp]

theorem Equiv.toHomeomorph_refl {X : Type u_1} [TopologicalSpace X] : (Equiv.refl X).toHomeomorph ⋯ = Homeomorph.refl X

@[simp]

theorem Equiv.toHomeomorph_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toHomeomorph he).symm = e.symm.toHomeomorph ⋯

theorem Equiv.toHomeomorph_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ Y) (f : Y ≃ Z) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (hf : ∀ (s : Set Z), IsOpen (⇑f ⁻¹' s) ↔ IsOpen s) : (e.trans f).toHomeomorph ⋯ = (e.toHomeomorph he).trans (f.toHomeomorph hf)

def Equiv.toHomeomorphOfIsInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : Topology.IsInducing ⇑f) : X ≃ₜ Y

An inducing equiv between topological spaces is a homeomorphism.

Equations

• f.toHomeomorphOfIsInducing hf = { toEquiv := f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Equiv.toHomeomorphOfIsInducing_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : Topology.IsInducing ⇑f) : (f.toHomeomorphOfIsInducing hf).toEquiv = f

@[deprecated Equiv.toHomeomorphOfIsInducing (since := "2024-10-28")]

def Equiv.toHomeomorphOfInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : Topology.IsInducing ⇑f) : X ≃ₜ Y

Alias of Equiv.toHomeomorphOfIsInducing.

---

An inducing equiv between topological spaces is a homeomorphism.

Equations

• @Equiv.toHomeomorphOfInducing = @Equiv.toHomeomorphOfIsInducing

def Equiv.toHomeomorphOfContinuousOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : X ≃ₜ Y

If a bijective map e : X ≃ Y is continuous and open, then it is a homeomorphism.

Equations

• e.toHomeomorphOfContinuousOpen h₁ h₂ = e.toHomeomorphOfIsInducing ⋯

@[simp]

theorem Equiv.toHomeomorphOfContinuousOpen_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : (e.toHomeomorphOfContinuousOpen h₁ h₂).toEquiv = e

@[deprecated Equiv.toHomeomorphOfContinuousOpen (since := "2025-04-16")]

def Homeomorph.homeomorphOfContinuousOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : X ≃ₜ Y

Alias of Equiv.toHomeomorphOfContinuousOpen.

---

If a bijective map e : X ≃ Y is continuous and open, then it is a homeomorphism.

Equations

• @Homeomorph.homeomorphOfContinuousOpen = @Equiv.toHomeomorphOfContinuousOpen

@[deprecated Equiv.toHomeomorphOfContinuousOpen_toEquiv (since := "2025-04-16")]

theorem Homeomorph.homeomorphOfContinuousOpen_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : (e.toHomeomorphOfContinuousOpen h₁ h₂).toEquiv = e

Alias of Equiv.toHomeomorphOfContinuousOpen_toEquiv.

@[simp]

theorem Equiv.toHomeomorphOfContinuousOpen_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂) = ⇑e

@[deprecated Equiv.toHomeomorphOfContinuousOpen_apply (since := "2025-04-16")]

theorem Homeomorph.homeomorphOfContinuousOpen_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂) = ⇑e

Alias of Equiv.toHomeomorphOfContinuousOpen_apply.

@[simp]

theorem Equiv.toHomeomorphOfContinuousOpen_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂).symm = ⇑e.symm

@[deprecated Equiv.toHomeomorphOfContinuousOpen_symm_apply (since := "2025-04-16")]

theorem Homeomorph.homeomorphOfContinuousOpen_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsOpenMap ⇑e) : ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂).symm = ⇑e.symm

Alias of Equiv.toHomeomorphOfContinuousOpen_symm_apply.

def Equiv.toHomeomorphOfContinuousClosed {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e) : X ≃ₜ Y

If a bijective map e : X ≃ Y is continuous and open, then it is a homeomorphism.

Equations

• e.toHomeomorphOfContinuousClosed h₁ h₂ = e.toHomeomorphOfIsInducing ⋯

@[simp]

theorem Equiv.toHomeomorphOfContinuousClosed_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e) : (e.toHomeomorphOfContinuousClosed h₁ h₂).toEquiv = e

@[deprecated Equiv.toHomeomorphOfContinuousClosed (since := "2025-04-16")]

def Homeomorph.homeomorphOfContinuousClosed {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e) : X ≃ₜ Y

Alias of Equiv.toHomeomorphOfContinuousClosed.

---

If a bijective map e : X ≃ Y is continuous and open, then it is a homeomorphism.

Equations

• @Homeomorph.homeomorphOfContinuousClosed = @Equiv.toHomeomorphOfContinuousClosed

@[simp]

theorem Equiv.toHomeomorphOfContinuousClosed_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e) : ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂) = ⇑e

@[simp]

theorem Equiv.toHomeomorphOfContinuousClosed_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e) : ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂).symm = ⇑e.symm

class HomeomorphClass (F : Type u_5) (A : outParam (Type u_6)) (B : outParam (Type u_7)) [TopologicalSpace A] [TopologicalSpace B] [h : EquivLike F A B] : Prop

HomeomorphClass F A B states that F is a type of homeomorphisms.

• map_continuous (f : F) : Continuous ⇑f
• inv_continuous (f : F) : Continuous (EquivLike.inv f)

def HomeomorphClass.toHomeomorph {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [h : HomeomorphClass F α β] (f : F) : α ≃ₜ β

Turn an element of a type F satisfying HomeomorphClass F α β into an actual Homeomorph. This is declared as the default coercion from F to α ≃ₜ β.

Equations

• ↑f = { toEquiv := ↑f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem HomeomorphClass.coe_coe {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [h : HomeomorphClass F α β] (f : F) : ⇑↑f = ⇑f

instance HomeomorphClass.instCoeOutHomeomorph {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [HomeomorphClass F α β] : CoeOut F (α ≃ₜ β)

Equations

• HomeomorphClass.instCoeOutHomeomorph = { coe := HomeomorphClass.toHomeomorph }

theorem HomeomorphClass.toHomeomorph_injective {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [HomeomorphClass F α β] : Function.Injective toHomeomorph

instance HomeomorphClass.instContinuousMapClass {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [HomeomorphClass F α β] : ContinuousMapClass F α β

instance HomeomorphClass.instHomeomorph {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] : HomeomorphClass (α ≃ₜ β) α β

structure IsHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

Predicate saying that f is a homeomorphism.

This should be used only when f is a concrete function whose continuous inverse is not easy to write down. Otherwise, Homeomorph should be preferred as it bundles the continuous inverse.

Having both Homeomorph and IsHomeomorph is justified by the fact that so many function properties are unbundled in the topology part of the library, and by the fact that a homeomorphism is not merely a continuous bijection, that is IsHomeomorph f is not equivalent to Continuous f ∧ Bijective f but to Continuous f ∧ Bijective f ∧ IsOpenMap f.

• continuous : Continuous f
• isOpenMap : IsOpenMap f
• bijective : Function.Bijective f

theorem Homeomorph.isHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsHomeomorph ⇑h

theorem IsHomeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : Function.Injective f

theorem IsHomeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : Function.Surjective f

theorem IsHomeomorph.id {X : Type u_1} [TopologicalSpace X] : IsHomeomorph id

theorem IsHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsHomeomorph g) (hf : IsHomeomorph f) : IsHomeomorph (g ∘ f)