Documentation

Mathlib.Topology.Homeomorph

Homeomorphisms #

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

Main definitions #

Main results #

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

Homeomorphism between X and Y, also called topological isomorphism

  • toFun : XY
  • invFun : YX
  • 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
    theorem Homeomorph.continuous_toFun {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] (self : X ≃ₜ Y) :
    Continuous self.toFun

    The forward map of a homeomorphism is a continuous function.

    theorem Homeomorph.continuous_invFun {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] (self : X ≃ₜ Y) :
    Continuous self.invFun

    The inverse map of a homeomorphism is a continuous function.

    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
      • Homeomorph.instEquivLike = { coe := fun (h : X ≃ₜ Y) => h.toEquiv, inv := fun (h : X ≃ₜ Y) => h.symm, left_inv := , right_inv := , coe_injective' := }
      instance Homeomorph.instCoeFunForall {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
      CoeFun (X ≃ₜ Y) fun (x : X ≃ₜ Y) => XY
      Equations
      • Homeomorph.instCoeFunForall = { coe := DFunLike.coe }
      @[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 := }
      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
        • h.symm = { toEquiv := h.symm, continuous_toFun := , continuous_invFun := }
        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_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {h : X ≃ₜ Y} {h' : X ≃ₜ Y} :
            h = h' ∀ (x : X), h x = h' x
            theorem Homeomorph.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {h : X ≃ₜ Y} {h' : X ≃ₜ Y} (H : ∀ (x : X), h x = h' x) :
            h = h'
            @[simp]

            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
              • h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, continuous_toFun := , continuous_invFun := }
              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) :
                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
                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
                • f.changeInv g hg = { toFun := f, invFun := g, left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
                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
                  @[simp]
                  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_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.inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                  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.quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                  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.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                  noncomputable def Homeomorph.ofEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : Embedding f) :
                  X ≃ₜ (Set.range f)

                  Homeomorphism given an embedding.

                  Equations
                  Instances For
                    @[simp]
                    theorem Homeomorph.isCompact_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) :

                    If h : X → Y is a homeomorphism, h(s) is compact iff s is.

                    @[simp]
                    theorem Homeomorph.isCompact_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) :

                    If h : X → Y is a homeomorphism, h⁻¹(s) is compact iff s is.

                    @[simp]
                    theorem Homeomorph.isSigmaCompact_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) :

                    If h : X → Y is a homeomorphism, s is σ-compact iff h(s) is.

                    @[simp]

                    If h : X → Y is a homeomorphism, h⁻¹(s) is σ-compact iff s is.

                    @[simp]
                    theorem Homeomorph.isPreconnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) :
                    @[simp]
                    @[simp]
                    theorem Homeomorph.isConnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) :
                    @[simp]
                    theorem Homeomorph.isConnected_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y) :
                    theorem Homeomorph.image_connectedComponentIn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x s) :
                    theorem Homeomorph.t0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y) :
                    theorem Homeomorph.t1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] (h : X ≃ₜ Y) :
                    theorem Homeomorph.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) :
                    theorem Homeomorph.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y) :
                    @[deprecated Homeomorph.isDenseEmbedding]
                    theorem Homeomorph.denseEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :

                    Alias of Homeomorph.isDenseEmbedding.

                    @[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.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space X] (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)
                    theorem HasCompactSupport.comp_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {M : Type u_7} [Zero M] {f : YM} (hf : HasCompactSupport f) (φ : X ≃ₜ Y) :
                    theorem HasCompactMulSupport.comp_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {M : Type u_7} [One M] {f : YM} (hf : HasCompactMulSupport f) (φ : X ≃ₜ Y) :
                    @[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)
                    @[simp]
                    theorem Homeomorph.map_punctured_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) :
                    Filter.map (⇑h) (nhdsWithin x {x}) = nhdsWithin (h x) {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)

                    If the codomain of a homeomorphism is a locally connected space, then the domain is also a locally connected space.

                    The codomain of a homeomorphism is a locally compact space if and only if the domain is a locally compact space.

                    @[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) :
                    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
                    Instances For
                      @[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) :
                      @[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) :
                      (Homeomorph.homeomorphOfContinuousOpen e h₁ h₂).symm = e.symm
                      @[simp]
                      theorem Homeomorph.comp_continuousOn_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : ZX) (s : Set Z) :
                      @[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)
                      theorem Homeomorph.comp_continuousWithinAt_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) (f : ZX) (s : Set Z) (z : Z) :
                      @[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} :
                      @[simp]
                      theorem Homeomorph.subtype_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x q (h x)) (a : { a : X // p a }) :
                      ((h.subtype h_iff) a) = h a
                      @[simp]
                      theorem Homeomorph.subtype_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x q (h x)) (b : { b : Y // q b }) :
                      ((h.subtype h_iff).symm b) = h.symm b
                      def Homeomorph.subtype {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x q (h x)) :
                      { x : X // p x } ≃ₜ { y : Y // q y }

                      A homeomorphism h : X ≃ₜ Y lifts to a homeomorphism between subtypes corresponding to predicates p : X → Prop and q : Y → Prop so long as p = q ∘ h.

                      Equations
                      • h.subtype h_iff = { toEquiv := h.subtypeEquiv h_iff, continuous_toFun := , continuous_invFun := }
                      Instances For
                        @[simp]
                        theorem Homeomorph.subtype_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : XProp} {q : YProp} (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x q (h x)) :
                        (h.subtype h_iff).toEquiv = h.subtypeEquiv h_iff
                        @[reducible, inline]
                        abbrev Homeomorph.sets {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (h : X ≃ₜ Y) (h_eq : s = h ⁻¹' t) :
                        s ≃ₜ t

                        A homeomorphism h : X ≃ₜ Y lifts to a homeomorphism between sets s : Set X and t : Set Y whenever h maps s onto t.

                        Equations
                        • h.sets h_eq = h.subtype
                        Instances For
                          def Homeomorph.setCongr {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (h : s = t) :
                          s ≃ₜ t

                          If two sets are equal, then they are homeomorphic.

                          Equations
                          Instances For
                            def Homeomorph.sumCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
                            X Y ≃ₜ X' Y'

                            Sum of two homeomorphisms.

                            Equations
                            • h₁.sumCongr h₂ = { toEquiv := h₁.sumCongr h₂.toEquiv, continuous_toFun := , continuous_invFun := }
                            Instances For
                              def Homeomorph.prodCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
                              X × Y ≃ₜ X' × Y'

                              Product of two homeomorphisms.

                              Equations
                              • h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, continuous_toFun := , continuous_invFun := }
                              Instances For
                                @[simp]
                                theorem Homeomorph.prodCongr_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
                                (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
                                @[simp]
                                theorem Homeomorph.coe_prodCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
                                (h₁.prodCongr h₂) = Prod.map h₁ h₂
                                def Homeomorph.sumComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] :
                                X Y ≃ₜ Y X

                                X ⊕ Y is homeomorphic to Y ⊕ X.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Homeomorph.coe_sumComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] :
                                  (Homeomorph.sumComm X Y) = Sum.swap
                                  def Homeomorph.sumAssoc (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                  (X Y) Z ≃ₜ X Y Z

                                  (X ⊕ Y) ⊕ Z is homeomorphic to X ⊕ (Y ⊕ Z).

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Homeomorph.sumAssoc_toEquiv (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                    (Homeomorph.sumAssoc X Y Z).toEquiv = Equiv.sumAssoc X Y Z
                                    def Homeomorph.sumSumSumComm (X : Type u_1) (Y : Type u_2) (W : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] :
                                    (X Y) W Z ≃ₜ (X W) Y Z

                                    Four-way commutativity of the disjoint union. The name matches add_add_add_comm.

                                    Equations
                                    Instances For
                                      @[simp]
                                      @[simp]
                                      theorem Homeomorph.sumEmpty_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] :
                                      (Homeomorph.sumEmpty X Y) = Sum.elim id fun (a : Y) => isEmptyElim a
                                      def Homeomorph.sumEmpty (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] :
                                      X Y ≃ₜ X

                                      The sum of X with any empty topological space is homeomorphic to X.

                                      Equations
                                      Instances For
                                        def Homeomorph.emptySum (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty Y] :
                                        Y X ≃ₜ X

                                        The sum of X with any empty topological space is homeomorphic to X.

                                        Equations
                                        Instances For
                                          @[simp]
                                          def Homeomorph.prodComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] :
                                          X × Y ≃ₜ Y × X

                                          X × Y is homeomorphic to Y × X.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Homeomorph.coe_prodComm (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] :
                                            (Homeomorph.prodComm X Y) = Prod.swap
                                            def Homeomorph.prodAssoc (X : Type u_1) (Y : Type u_2) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                            (X × Y) × Z ≃ₜ X × Y × Z

                                            (X × Y) × Z is homeomorphic to X × (Y × Z).

                                            Equations
                                            Instances For
                                              @[simp]
                                              def Homeomorph.prodProdProdComm (X : Type u_1) (Y : Type u_2) (W : Type u_3) (Z : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace W] [TopologicalSpace Z] :
                                              (X × Y) × W × Z ≃ₜ (X × W) × Y × Z

                                              Four-way commutativity of prod. The name matches mul_mul_mul_comm.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem Homeomorph.prodPUnit_apply (X : Type u_1) [TopologicalSpace X] :
                                                (Homeomorph.prodPUnit X) = fun (p : X × PUnit.{u_7 + 1} ) => p.1

                                                X × {*} is homeomorphic to X.

                                                Equations
                                                Instances For

                                                  {*} × X is homeomorphic to X.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    @[simp]
                                                    theorem Homeomorph.homeomorphOfUnique_symm_apply (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] [Unique Y] :
                                                    ∀ (a : Y), (Homeomorph.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), (Homeomorph.homeomorphOfUnique X Y) a = default

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

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Homeomorph.piCongrLeft_apply {ι : Type u_7} {ι' : Type u_8} {Y : ι'Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ι') :
                                                      ∀ (a : (b : ι) → Y (e.symm.symm b)) (a_1 : ι'), (Homeomorph.piCongrLeft e) a a_1 = (Equiv.piCongrLeft' Y e.symm).symm a a_1
                                                      @[simp]
                                                      theorem Homeomorph.piCongrLeft_toEquiv {ι : Type u_7} {ι' : Type u_8} {Y : ι'Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ι') :
                                                      def Homeomorph.piCongrLeft {ι : Type u_7} {ι' : Type u_8} {Y : ι'Type u_9} [(j : ι') → TopologicalSpace (Y j)] (e : ι ι') :
                                                      ((i : ι) → Y (e i)) ≃ₜ ((j : ι') → Y j)

                                                      Equiv.piCongrLeft as a homeomorphism: this is the natural homeomorphism Π i, Y (e i) ≃ₜ Π j, Y j obtained from a bijection ι ≃ ι'.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem Homeomorph.piCongrRight_apply {ι : Type u_7} {Y₁ : ιType u_8} {Y₂ : ιType u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) (H : (a : ι) → Y₁ a) (a : ι) :
                                                        (Homeomorph.piCongrRight F) H a = (F a) (H a)
                                                        @[simp]
                                                        theorem Homeomorph.piCongrRight_toEquiv {ι : Type u_7} {Y₁ : ιType u_8} {Y₂ : ιType u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) :
                                                        (Homeomorph.piCongrRight F).toEquiv = Equiv.piCongrRight fun (i : ι) => (F i).toEquiv
                                                        def Homeomorph.piCongrRight {ι : Type u_7} {Y₁ : ιType u_8} {Y₂ : ιType u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) :
                                                        ((i : ι) → Y₁ i) ≃ₜ ((i : ι) → Y₂ i)

                                                        Equiv.piCongrRight as a homeomorphism: this is the natural homeomorphism Π i, Y₁ i ≃ₜ Π j, Y₂ i obtained from homeomorphisms Y₁ i ≃ₜ Y₂ i for each i.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Homeomorph.piCongrRight_symm {ι : Type u_7} {Y₁ : ιType u_8} {Y₂ : ιType u_9} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) :
                                                          (Homeomorph.piCongrRight F).symm = Homeomorph.piCongrRight fun (i : ι) => (F i).symm
                                                          @[simp]
                                                          theorem Homeomorph.piCongr_apply {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁Type u_9} {Y₂ : ι₂Type u_10} [(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) :
                                                          ∀ (a : (i : ι₁) → Y₁ i) (i₂ : ι₂), (Homeomorph.piCongr e F) a i₂ = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv) a (e.symm i₂)
                                                          @[simp]
                                                          theorem Homeomorph.piCongr_toEquiv {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁Type u_9} {Y₂ : ι₂Type u_10} [(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) :
                                                          (Homeomorph.piCongr e F).toEquiv = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv).trans (Equiv.piCongrLeft Y₂ e)
                                                          def Homeomorph.piCongr {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁Type u_9} {Y₂ : ι₂Type u_10} [(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)) :
                                                          ((i₁ : ι₁) → Y₁ i₁) ≃ₜ ((i₂ : ι₂) → Y₂ i₂)

                                                          Equiv.piCongr as a homeomorphism: this is the natural homeomorphism Π i₁, Y₁ i ≃ₜ Π i₂, Y₂ i₂ obtained from a bijection ι₁ ≃ ι₂ and homeomorphisms Y₁ i₁ ≃ₜ Y₂ (e i₁) for each i₁ : ι₁.

                                                          Equations
                                                          Instances For

                                                            ULift X is homeomorphic to X.

                                                            Equations
                                                            • Homeomorph.ulift = { toEquiv := Equiv.ulift, continuous_toFun := , continuous_invFun := }
                                                            Instances For
                                                              @[simp]
                                                              theorem Homeomorph.sumProdDistrib_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                                              ∀ (a : X × Z Y × Z), Homeomorph.sumProdDistrib.symm a = (Equiv.sumProdDistrib X Y Z).symm a
                                                              @[simp]
                                                              theorem Homeomorph.sumProdDistrib_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                                              ∀ (a : (X Y) × Z), Homeomorph.sumProdDistrib a = (Equiv.sumProdDistrib X Y Z) a
                                                              def Homeomorph.sumProdDistrib {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                                              (X Y) × Z ≃ₜ X × Z Y × Z

                                                              (X ⊕ Y) × Z is homeomorphic to X × Z ⊕ Y × Z.

                                                              Equations
                                                              Instances For
                                                                def Homeomorph.prodSumDistrib {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                                                X × (Y Z) ≃ₜ X × Y X × Z

                                                                X × (Y ⊕ Z) is homeomorphic to X × Y ⊕ X × Z.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Homeomorph.sigmaProdDistrib_apply {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ιType u_8} [(i : ι) → TopologicalSpace (X i)] :
                                                                  ∀ (a : ((i : ι) × X i) × Y), Homeomorph.sigmaProdDistrib a = a.1.fst, (a.1.snd, a.2)
                                                                  @[simp]
                                                                  theorem Homeomorph.sigmaProdDistrib_symm_apply {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ιType u_8} [(i : ι) → TopologicalSpace (X i)] :
                                                                  ∀ (a : (i : ι) × X i × Y), Homeomorph.sigmaProdDistrib.symm a = (a.fst, a.snd.1, a.snd.2)
                                                                  @[simp]
                                                                  theorem Homeomorph.sigmaProdDistrib_toEquiv {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ιType u_8} [(i : ι) → TopologicalSpace (X i)] :
                                                                  Homeomorph.sigmaProdDistrib.toEquiv = Equiv.sigmaProdDistrib X Y
                                                                  def Homeomorph.sigmaProdDistrib {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_7} {X : ιType u_8} [(i : ι) → TopologicalSpace (X i)] :
                                                                  ((i : ι) × X i) × Y ≃ₜ (i : ι) × X i × Y

                                                                  (Σ i, X i) × Y is homeomorphic to Σ i, (X i × Y).

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem Homeomorph.funUnique_symm_apply (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] :
                                                                    (Homeomorph.funUnique ι X).symm = uniqueElim
                                                                    @[simp]
                                                                    theorem Homeomorph.funUnique_apply (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] :
                                                                    (Homeomorph.funUnique ι X) = fun (f : ιX) => f default
                                                                    def Homeomorph.funUnique (ι : Type u_7) (X : Type u_8) [Unique ι] [TopologicalSpace X] :
                                                                    (ιX) ≃ₜ X

                                                                    If ι has a unique element, then ι → X is homeomorphic to X.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Homeomorph.piFinTwo_apply (X : Fin 2Type u) [(i : Fin 2) → TopologicalSpace (X i)] :
                                                                      (Homeomorph.piFinTwo X) = fun (f : (i : Fin 2) → X i) => (f 0, f 1)
                                                                      @[simp]
                                                                      theorem Homeomorph.piFinTwo_symm_apply (X : Fin 2Type u) [(i : Fin 2) → TopologicalSpace (X i)] :
                                                                      (Homeomorph.piFinTwo X).symm = fun (p : X 0 × X 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                                                                      def Homeomorph.piFinTwo (X : Fin 2Type u) [(i : Fin 2) → TopologicalSpace (X i)] :
                                                                      ((i : Fin 2) → X i) ≃ₜ X 0 × X 1

                                                                      Homeomorphism between dependent functions Π i : Fin 2, X i and X 0 × X 1.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem Homeomorph.finTwoArrow_apply {X : Type u_1} [TopologicalSpace X] :
                                                                        Homeomorph.finTwoArrow = fun (f : Fin 2X) => (f 0, f 1)
                                                                        @[simp]
                                                                        theorem Homeomorph.finTwoArrow_symm_apply {X : Type u_1} [TopologicalSpace X] :
                                                                        Homeomorph.finTwoArrow.symm = fun (x : X × X) => ![x.1, x.2]
                                                                        def Homeomorph.finTwoArrow {X : Type u_1} [TopologicalSpace X] :
                                                                        (Fin 2X) ≃ₜ X × X

                                                                        Homeomorphism between X² = Fin 2 → X and X × X.

                                                                        Equations
                                                                        • Homeomorph.finTwoArrow = { toEquiv := finTwoArrowEquiv X, continuous_toFun := , continuous_invFun := }
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Homeomorph.image_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (x : s) :
                                                                          ((e.image s) x) = e x
                                                                          @[simp]
                                                                          theorem Homeomorph.image_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (y : (e.toEquiv '' s)) :
                                                                          ((e.image s).symm y) = e.symm y
                                                                          def Homeomorph.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) :
                                                                          s ≃ₜ (e '' s)

                                                                          A subset of a topological space is homeomorphic to its image under a homeomorphism.

                                                                          Equations
                                                                          • e.image s = { toEquiv := e.image s, continuous_toFun := , continuous_invFun := }
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Homeomorph.Set.univ_apply (X : Type u_7) [TopologicalSpace X] :
                                                                            (Homeomorph.Set.univ X) = Subtype.val
                                                                            @[simp]
                                                                            theorem Homeomorph.Set.univ_symm_apply_coe (X : Type u_7) [TopologicalSpace X] (a : X) :
                                                                            ((Homeomorph.Set.univ X).symm a) = a
                                                                            def Homeomorph.Set.univ (X : Type u_7) [TopologicalSpace X] :
                                                                            Set.univ ≃ₜ X

                                                                            Set.univ X is homeomorphic to X.

                                                                            Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem Homeomorph.Set.prod_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) (x : { c : X × Y // s c.1 t c.2 }) :
                                                                              (Homeomorph.Set.prod s t) x = ((↑x).1, , (↑x).2, )
                                                                              @[simp]
                                                                              theorem Homeomorph.Set.prod_symm_apply_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) (x : { a : X // s a } × { b : Y // t b }) :
                                                                              ((Homeomorph.Set.prod s t).symm x) = (x.1, x.2)
                                                                              def Homeomorph.Set.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) :
                                                                              (s ×ˢ t) ≃ₜ s × t

                                                                              s ×ˢ t is homeomorphic to s × t.

                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem Homeomorph.piEquivPiSubtypeProd_apply {ι : Type u_7} (p : ιProp) (Y : ιType u_8) [(i : ι) → TopologicalSpace (Y i)] [DecidablePred p] (f : (i : ι) → Y i) :
                                                                                (Homeomorph.piEquivPiSubtypeProd p Y) f = (fun (x : { x : ι // p x }) => f x, fun (x : { x : ι // ¬p x }) => f x)
                                                                                @[simp]
                                                                                theorem Homeomorph.piEquivPiSubtypeProd_symm_apply {ι : Type u_7} (p : ιProp) (Y : ιType u_8) [(i : ι) → TopologicalSpace (Y i)] [DecidablePred p] (f : ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i)) (x : ι) :
                                                                                (Homeomorph.piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 x, h else f.2 x, h
                                                                                def Homeomorph.piEquivPiSubtypeProd {ι : Type u_7} (p : ιProp) (Y : ιType u_8) [(i : ι) → TopologicalSpace (Y i)] [DecidablePred p] :
                                                                                ((i : ι) → Y i) ≃ₜ ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i)

                                                                                The topological space Π i, Y i can be split as a product by separating the indices in ι depending on whether they satisfy a predicate p or not.

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem Homeomorph.piSplitAt_apply {ι : Type u_7} [DecidableEq ι] (i : ι) (Y : ιType u_8) [(j : ι) → TopologicalSpace (Y j)] (f : (j : ι) → Y j) :
                                                                                  (Homeomorph.piSplitAt i Y) f = (f i, fun (j : { j : ι // ¬j = i }) => f j)
                                                                                  @[simp]
                                                                                  theorem Homeomorph.piSplitAt_symm_apply {ι : Type u_7} [DecidableEq ι] (i : ι) (Y : ιType u_8) [(j : ι) → TopologicalSpace (Y j)] (f : Y i × ((j : { j : ι // j i }) → Y j)) (j : ι) :
                                                                                  (Homeomorph.piSplitAt i Y).symm f j = if h : j = i then f.1 else f.2 j, h
                                                                                  def Homeomorph.piSplitAt {ι : Type u_7} [DecidableEq ι] (i : ι) (Y : ιType u_8) [(j : ι) → TopologicalSpace (Y j)] :
                                                                                  ((j : ι) → Y j) ≃ₜ Y i × ((j : { j : ι // j i }) → Y j)

                                                                                  A product of topological spaces can be split as the binary product of one of the spaces and the product of all the remaining spaces.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem Homeomorph.funSplitAt_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_7} [DecidableEq ι] (i : ι) (f : (j : ι) → (fun (a : ι) => Y) j) :
                                                                                    (Homeomorph.funSplitAt Y i) f = (f i, fun (j : { j : ι // ¬j = i }) => f j)
                                                                                    @[simp]
                                                                                    theorem Homeomorph.funSplitAt_symm_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_7} [DecidableEq ι] (i : ι) (f : (fun (a : ι) => Y) i × ((j : { j : ι // j i }) → (fun (a : ι) => Y) j)) (j : ι) :
                                                                                    (Homeomorph.funSplitAt Y i).symm f j = if h : j = i then f.1 else f.2 j,
                                                                                    def Homeomorph.funSplitAt (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_7} [DecidableEq ι] (i : ι) :
                                                                                    (ιY) ≃ₜ Y × ({ j : ι // j i }Y)

                                                                                    A product of copies of a topological space can be split as the binary product of one copy and the product of all the remaining copies.

                                                                                    Equations
                                                                                    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) :
                                                                                      (e.toHomeomorph he).toEquiv = e
                                                                                      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 equiv between topological spaces respecting openness is a homeomorphism.

                                                                                      Equations
                                                                                      • e.toHomeomorph he = { toEquiv := e, continuous_toFun := , continuous_invFun := }
                                                                                      Instances For
                                                                                        @[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)
                                                                                        @[simp]
                                                                                        theorem Equiv.toHomeomorphOfInducing_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X Y) (hf : Inducing f) :
                                                                                        (f.toHomeomorphOfInducing hf).toEquiv = f
                                                                                        def Equiv.toHomeomorphOfInducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X Y) (hf : Inducing f) :
                                                                                        X ≃ₜ Y

                                                                                        An inducing equiv between topological spaces is a homeomorphism.

                                                                                        Equations
                                                                                        • f.toHomeomorphOfInducing hf = { toEquiv := f, continuous_toFun := , continuous_invFun := }
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem Continuous.homeoOfEquivCompactToT2_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X Y} (hf : Continuous f) :
                                                                                          hf.homeoOfEquivCompactToT2.toEquiv = f
                                                                                          def Continuous.homeoOfEquivCompactToT2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X Y} (hf : Continuous f) :
                                                                                          X ≃ₜ Y

                                                                                          Continuous equivalences from a compact space to a T2 space are homeomorphisms.

                                                                                          This is not true when T2 is weakened to T1 (see Continuous.homeoOfEquivCompactToT2.t1_counterexample).

                                                                                          Equations
                                                                                          • hf.homeoOfEquivCompactToT2 = { toEquiv := f, continuous_toFun := hf, continuous_invFun := }
                                                                                          Instances For
                                                                                            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 IsHomeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (self : IsHomeomorph f) :
                                                                                              theorem IsHomeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (self : IsHomeomorph f) :
                                                                                              theorem IsHomeomorph.bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (self : IsHomeomorph f) :
                                                                                              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) :
                                                                                              @[simp]
                                                                                              theorem IsHomeomorph.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : IsHomeomorph f) :
                                                                                              ∀ (a : X), (IsHomeomorph.homeomorph f hf) a = f a
                                                                                              @[simp]
                                                                                              theorem IsHomeomorph.homeomorph_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : IsHomeomorph f) :
                                                                                              @[simp]
                                                                                              theorem IsHomeomorph.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : IsHomeomorph f) (b : Y) :
                                                                                              noncomputable def IsHomeomorph.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (hf : IsHomeomorph f) :
                                                                                              X ≃ₜ Y

                                                                                              Bundled homeomorphism constructed from a map that is a homeomorphism.

                                                                                              Equations
                                                                                              Instances For
                                                                                                theorem IsHomeomorph.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                                                theorem IsHomeomorph.inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                                                theorem IsHomeomorph.quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                                                theorem IsHomeomorph.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                                                theorem IsHomeomorph.openEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                                                theorem IsHomeomorph.closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :
                                                                                                @[deprecated IsHomeomorph.isDenseEmbedding]
                                                                                                theorem IsHomeomorph.denseEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsHomeomorph f) :

                                                                                                Alias of IsHomeomorph.isDenseEmbedding.

                                                                                                theorem isHomeomorph_iff_exists_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} :
                                                                                                IsHomeomorph f ∃ (h : X ≃ₜ Y), h = f

                                                                                                A map is a homeomorphism iff it is the map underlying a bundled homeomorphism h : X ≃ₜ Y.

                                                                                                A map is a homeomorphism iff it is continuous and has a continuous inverse.

                                                                                                A map is a homeomorphism iff it is a surjective embedding.

                                                                                                A map is a homeomorphism iff it is continuous, closed and bijective.

                                                                                                A map from a compact space to a T2 space is a homeomorphism iff it is continuous and bijective.

                                                                                                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) :
                                                                                                theorem IsHomeomorph.sumMap {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {W : Type u_5} [TopologicalSpace W] {f : XY} {g : ZW} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :
                                                                                                theorem IsHomeomorph.prodMap {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {W : Type u_5} [TopologicalSpace W] {f : XY} {g : ZW} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :
                                                                                                theorem IsHomeomorph.sigmaMap {ι : Type u_6} {κ : Type u_7} {X : ιType u_8} {Y : κType u_9} [(i : ι) → TopologicalSpace (X i)] [(i : κ) → TopologicalSpace (Y i)] {f : ικ} (hf : Function.Bijective f) {g : (i : ι) → X iY (f i)} (hg : ∀ (i : ι), IsHomeomorph (g i)) :
                                                                                                theorem IsHomeomorph.pi_map {ι : Type u_6} {X : ιType u_7} {Y : ιType u_8} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f : (i : ι) → X iY i} (h : ∀ (i : ι), IsHomeomorph (f i)) :
                                                                                                IsHomeomorph fun (x : (i : ι) → X i) (i : ι) => f i (x i)