Documentation

Mathlib.Topology.Homeomorph.Defs

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 #

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

Instances For

    Homeomorphism between X and Y, also called topological isomorphism

    Equations
      Instances For
        instance Homeomorph.instEquivLike {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
        EquivLike (X ≃ₜ Y) X Y
        Equations
          @[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
            Instances For
              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
                Instances For
                  @[simp]
                  theorem Homeomorph.symm_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                  h.symm.symm = h
                  def Homeomorph.Simps.symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                  YX

                  See Note [custom simps projection]

                  Equations
                    Instances For
                      @[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

                      Identity map as a homeomorphism.

                      Equations
                        Instances For
                          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
                            Instances For
                              @[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
                              theorem Homeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                              @[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]
                              @[simp]
                              def Homeomorph.changeInv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (g : YX) (hg : Function.RightInverse g f) :
                              X ≃ₜ Y

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

                              Equations
                                Instances For
                                  @[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) :
                                  theorem Homeomorph.image_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                                  @[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)
                                  @[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) :

                                  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✝¹
                                  @[deprecated Homeomorph.isQuotientMap (since := "2024-10-22")]

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

                                  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) :
                                  @[simp]
                                  theorem Homeomorph.isClosed_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y} :
                                  @[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) :
                                  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 : ZX} :
                                  @[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 : YZ} :
                                  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 : ZX) (z : 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 : YZ) (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 : ZX} :
                                  @[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 : YZ} :

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

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem Homeomorph.homeomorphOfUnique_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] (a✝ : X) :
                                      @[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
                                        Instances For
                                          @[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) :
                                          @[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_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) :
                                          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) :
                                          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
                                            Instances For
                                              @[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
                                                Instances For
                                                  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
                                                    Instances For
                                                      @[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) :
                                                      @[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
                                                        Instances For
                                                          @[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) :

                                                          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
                                                            Instances For
                                                              @[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) :
                                                              @[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
                                                                Instances For
                                                                  @[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) :
                                                                  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] :

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

                                                                  Instances
                                                                    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
                                                                      Instances For
                                                                        @[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
                                                                          instance HomeomorphClass.instContinuousMapClass {F : Type u_5} {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [EquivLike F α β] [HomeomorphClass F α β] :
                                                                          structure IsHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) :

                                                                          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.

                                                                          Instances For
                                                                            theorem Homeomorph.isHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                                                                            theorem IsHomeomorph.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                            theorem IsHomeomorph.surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                            theorem IsHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} {g : YZ} (hg : IsHomeomorph g) (hf : IsHomeomorph f) :