# 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

source
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.

Instances For

source
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))

Instances For

source
theorem Homeomorph.toEquiv_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
Function.Injective toEquiv
source
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' := ⋯ }

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

Instances For

source
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 := ⋯ }

Instances For

source
@[simp]
theorem Homeomorph.symm_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
h.symm.symm = h
source
theorem Homeomorph.symm_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
Function.Bijective Homeomorph.symm
source
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

Instances For

source
@[simp]
theorem Homeomorph.coe_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
⇑h.toEquiv = ⇑h
source
@[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
source
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'
source
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
source
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 := ⋯ }

Instances For

source
@[simp]
theorem Homeomorph.refl_apply (X : Type u_7) [TopologicalSpace X] :
⇑(Homeomorph.refl X) = id
source
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 := ⋯ }

Instances For

source
@[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)
source
@[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)
source
@[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
source
@[simp]
theorem Homeomorph.refl_symm {X : Type u_1} [TopologicalSpace X] :
(Homeomorph.refl X).symm = Homeomorph.refl X
source
theorem Homeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Continuous ⇑h
source
theorem Homeomorph.continuous_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Continuous ⇑h.symm
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem Homeomorph.bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Function.Bijective ⇑h
source
theorem Homeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Function.Injective ⇑h
source
theorem Homeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Function.Surjective ⇑h
source
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 := ⋯ }

Instances For

source
@[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
source
@[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
source
theorem Homeomorph.range_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Set.range ⇑h = Set.univ
source
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
source
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
source
@[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
source
@[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
source
theorem Homeomorph.image_eq_preimage_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) :
⇑h '' s = ⇑h.symm ⁻¹' s
source
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)ᶜ
source
theorem Homeomorph.isInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Topology.IsInducing ⇑h
source
theorem Homeomorph.induced_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
TopologicalSpace.induced (⇑h) inst✝ = inst✝¹
source
theorem Homeomorph.isQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Topology.IsQuotientMap ⇑h
source
theorem Homeomorph.coinduced_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
TopologicalSpace.coinduced (⇑h) inst✝ = inst✝¹
source
theorem Homeomorph.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Topology.IsEmbedding ⇑h
source
theorem Homeomorph.discreteTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [DiscreteTopology X] (h : X ≃ₜ Y) :
DiscreteTopology Y
source
theorem Homeomorph.discreteTopology_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
DiscreteTopology X ↔ DiscreteTopology Y
source
@[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
source
@[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
source
theorem Homeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
IsOpenMap ⇑h
source
theorem Homeomorph.isOpenQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
IsOpenQuotientMap ⇑h
source
@[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
source
@[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
source
theorem Homeomorph.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
IsClosedMap ⇑h
source
theorem Homeomorph.isOpenEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Topology.IsOpenEmbedding ⇑h
source
theorem Homeomorph.isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
Topology.IsClosedEmbedding ⇑h
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
@[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
source
@[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
source
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
source
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)
source
@[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
source
@[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
source
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 := ⋯ }

Instances For

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

Instances For

source
@[simp]
theorem Equiv.toEquiv_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).toEquiv = e
source
@[deprecated Equiv.toEquiv_toHomeomorph (since := "2025-10-09")]
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

Alias of `Equiv.toEquiv_toHomeomorph`.

source
@[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
source
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
source
@[simp]
theorem Equiv.toHomeomorph_refl {X : Type u_1} [TopologicalSpace X] :
(Equiv.refl X).toHomeomorph ⋯ = Homeomorph.refl X
source
@[simp]
theorem Equiv.symm_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).symm = e.symm.toHomeomorph ⋯
source
@[deprecated Equiv.symm_toHomeomorph (since := "2025-10-09")]
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 ⋯

Alias of `Equiv.symm_toHomeomorph`.

source
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)
source
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 := ⋯ }

Instances For

source
@[simp]
theorem Equiv.toEquiv_toHomeomorphOfIsInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : Topology.IsInducing ⇑f) :
(f.toHomeomorphOfIsInducing hf).toEquiv = f
source
@[simp]
theorem Equiv.toHomeomorphOfIsInducing_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : Topology.IsInducing ⇑f) :
⇑(f.toHomeomorphOfIsInducing hf) = ⇑f
source
@[simp]
theorem Equiv.toHomeomorphOfIsInducing_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ Y) (hf : Topology.IsInducing ⇑f) :
⇑(f.toHomeomorphOfIsInducing hf).symm = ⇑f.symm
source
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 ⋯

Instances For

source
@[simp]
theorem Equiv.toEquiv_toHomeomorphOfContinuousOpen {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
source
@[deprecated Equiv.toEquiv_toHomeomorphOfContinuousOpen (since := "2025-10-09")]
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

Alias of `Equiv.toEquiv_toHomeomorphOfContinuousOpen`.

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

Instances For

source
@[simp]
theorem Equiv.toEquiv_toHomeomorphOfContinuousClosed {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
source
@[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
source
@[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
source
def Equiv.toHomeomorphOfDiscrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [DiscreteTopology X] [TopologicalSpace Y] [DiscreteTopology Y] (e : X ≃ Y) :
X ≃ₜ Y

Any bijection between discrete spaces is a homeomorphism.

Equations

- e.toHomeomorphOfDiscrete = e.toHomeomorph ⋯

Instances For

source
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)

Instances

source
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 := ⋯ }

Instances For

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

source
theorem HomeomorphClass.toHomeomorph_injective {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [HomeomorphClass F α β] :
Function.Injective toHomeomorph
source
instance HomeomorphClass.instContinuousMapClass {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [HomeomorphClass F α β] :
ContinuousMapClass F α β
source
instance HomeomorphClass.instHomeomorph {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] :
HomeomorphClass (α ≃ₜ β) α β
source
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

Instances For

source
theorem Homeomorph.isHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
IsHomeomorph ⇑h
source
theorem IsHomeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) :
Function.Injective f
source
theorem IsHomeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) :
Function.Surjective f
source
theorem IsHomeomorph.id {X : Type u_1} [TopologicalSpace X] :
IsHomeomorph id
source
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)