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.

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'

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.

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

@[deprecated Homeomorph.isOpenEmbedding (since := "2024-10-18")]

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

Alias of Homeomorph.isOpenEmbedding.

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

@[deprecated Homeomorph.isClosedEmbedding (since := "2024-10-20")]

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

Alias of Homeomorph.isClosedEmbedding.

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)

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

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

Equations

• Homeomorph.homeomorphOfContinuousOpen e h₁ h₂ = { toEquiv := e, continuous_toFun := h₁, continuous_invFun := ⋯ }

@[simp]

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) : (homeomorphOfContinuousOpen e h₁ h₂).toEquiv = e

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

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

Equations

• Homeomorph.homeomorphOfContinuousClosed e h₁ h₂ = { toEquiv := e, continuous_toFun := h₁, continuous_invFun := ⋯ }

@[simp]

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) : ⇑(homeomorphOfContinuousOpen e h₁ h₂) = ⇑e

@[simp]

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) : ⇑(homeomorphOfContinuousOpen e h₁ h₂).symm = ⇑e.symm

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

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

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