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_4) (Y : Type u_5) [TopologicalSpace X] [TopologicalSpace Y] extends Equiv :
Type (max u_4 u_5)

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

    Homeomorphism between X and Y, also called topological isomorphism

    Equations
    Instances For
      Equations
      • Homeomorph.instEquivLikeHomeomorph = { coe := fun (h : X ≃ₜ Y) => h.toEquiv, inv := fun (h : X ≃ₜ Y) => h.symm, left_inv := , right_inv := , coe_injective' := }
      instance Homeomorph.instCoeFunHomeomorphForAll {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
      CoeFun (X ≃ₜ Y) fun (x : X ≃ₜ Y) => XY
      Equations
      • Homeomorph.instCoeFunHomeomorphForAll = { 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 = let __spread.0 := Equiv.equivOfIsEmpty X Y; { toEquiv := __spread.0, 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
        • Homeomorph.symm h = { toEquiv := h.symm, continuous_toFun := , continuous_invFun := }
        Instances For
          @[simp]
          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 = (Homeomorph.symm h)
            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_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) :
              X ≃ₜ Z

              Composition of two homeomorphisms.

              Equations
              • Homeomorph.trans h₁ 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_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) (x : X) :
                (Homeomorph.trans h₁ h₂) x = h₂ (h₁ x)
                @[simp]
                theorem Homeomorph.symm_trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X ≃ₜ Y) (g : Y ≃ₜ Z) (z : 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) :
                (Homeomorph.symm { toEquiv := a, continuous_toFun := b, continuous_invFun := c }) = 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 ((Homeomorph.symm h) 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) :
                (Homeomorph.symm h) (h x) = x
                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
                • Homeomorph.changeInv f g hg = { toEquiv := { 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) :
                  (Homeomorph.symm h) h = id
                  @[simp]
                  theorem Homeomorph.self_comp_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                  h (Homeomorph.symm h) = 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
                  @[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) :
                    @[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_6} [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_6} [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 ((Homeomorph.symm h)) (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) :

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

                    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.comp_continuousOn_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h : X ≃ₜ Y) {f : YZ} :
                      @[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 }) :
                      @[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 // (fun (a : X) => p a) a }) :
                      ((Homeomorph.subtype h h_iff) a) = h a
                      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
                      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)) :
                        (Homeomorph.subtype h h_iff).toEquiv = Equiv.subtypeEquiv h.toEquiv h_iff
                        @[inline, reducible]
                        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
                        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_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
                            X Y ≃ₜ X' Y'

                            Sum of two homeomorphisms.

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

                              Product of two homeomorphisms.

                              Equations
                              Instances For
                                @[simp]
                                theorem Homeomorph.prodCongr_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
                                @[simp]
                                theorem Homeomorph.coe_prodCongr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
                                (Homeomorph.prodCongr h₁ h₂) = Prod.map h₁ h₂
                                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_3) [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.prodPUnit_apply (X : Type u_1) [TopologicalSpace X] :
                                    (Homeomorph.prodPUnit X) = fun (p : X × PUnit.{u_6 + 1} ) => p.1

                                    X × {*} is homeomorphic to X.

                                    Equations
                                    Instances For
                                      @[simp]
                                      @[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_toEquiv {ι : Type u_6} {ι' : Type u_7} {Y : ι'Type u_8} [(j : ι') → TopologicalSpace (Y j)] (e : ι ι') :
                                        @[simp]
                                        theorem Homeomorph.piCongrLeft_apply {ι : Type u_6} {ι' : Type u_7} {Y : ι'Type u_8} [(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
                                        def Homeomorph.piCongrLeft {ι : Type u_6} {ι' : Type u_7} {Y : ι'Type u_8} [(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_6} {Y₁ : ιType u_7} {Y₂ : ιType u_8} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) (H : (a : ι) → (fun (i : ι) => Y₁ i) a) (a : ι) :
                                          (Homeomorph.piCongrRight F) H a = (F a) (H a)
                                          @[simp]
                                          theorem Homeomorph.piCongrRight_toEquiv {ι : Type u_6} {Y₁ : ιType u_7} {Y₂ : ιType u_8} [(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_6} {Y₁ : ιType u_7} {Y₂ : ιType u_8} [(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_6} {Y₁ : ιType u_7} {Y₂ : ιType u_8} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) :
                                            @[simp]
                                            theorem Homeomorph.piCongr_apply {ι₁ : Type u_6} {ι₂ : Type u_7} {Y₁ : ι₁Type u_8} {Y₂ : ι₂Type u_9} [(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_6} {ι₂ : Type u_7} {Y₁ : ι₁Type u_8} {Y₂ : ι₂Type u_9} [(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_6} {ι₂ : Type u_7} {Y₁ : ι₁Type u_8} {Y₂ : ι₂Type u_9} [(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
                                                def Homeomorph.sumProdDistrib {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [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_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] :
                                                  X × (Y Z) ≃ₜ X × Y X × Z

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

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Homeomorph.sigmaProdDistrib {Y : Type u_2} [TopologicalSpace Y] {ι : Type u_6} {X : ιType u_7} [(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_apply (ι : Type u_6) (X : Type u_7) [Unique ι] [TopologicalSpace X] :
                                                      (Homeomorph.funUnique ι X) = fun (f : ιX) => f default
                                                      @[simp]
                                                      theorem Homeomorph.funUnique_symm_apply (ι : Type u_6) (X : Type u_7) [Unique ι] [TopologicalSpace X] :
                                                      (Homeomorph.symm (Homeomorph.funUnique ι X)) = uniqueElim
                                                      def Homeomorph.funUnique (ι : Type u_6) (X : Type u_7) [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.symm (Homeomorph.piFinTwo X)) = 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_symm_apply {X : Type u_1} [TopologicalSpace X] :
                                                          (Homeomorph.symm Homeomorph.finTwoArrow) = fun (x : X × X) => ![x.1, x.2]
                                                          @[simp]
                                                          theorem Homeomorph.finTwoArrow_apply {X : Type u_1} [TopologicalSpace X] :
                                                          Homeomorph.finTwoArrow = fun (f : Fin 2X) => (f 0, f 1)
                                                          def Homeomorph.finTwoArrow {X : Type u_1} [TopologicalSpace X] :
                                                          (Fin 2X) ≃ₜ X × X

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

                                                          Equations
                                                          Instances For
                                                            @[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)) :
                                                            @[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) :
                                                            ((Homeomorph.image e s) x) = e x
                                                            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
                                                            Instances For
                                                              @[simp]
                                                              theorem Homeomorph.Set.univ_apply (X : Type u_6) [TopologicalSpace X] :
                                                              (Homeomorph.Set.univ X) = Subtype.val
                                                              def Homeomorph.Set.univ (X : Type u_6) [TopologicalSpace X] :
                                                              Set.univ ≃ₜ X

                                                              Set.univ X is homeomorphic to X.

                                                              Equations
                                                              Instances For
                                                                @[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.symm (Homeomorph.Set.prod s t)) x) = (x.1, x.2)
                                                                @[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 = ({ val := (x).1, property := }, { val := (x).2, property := })
                                                                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_6} (p : ιProp) (Y : ιType u_7) [(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_6} (p : ιProp) (Y : ιType u_7) [(i : ι) → TopologicalSpace (Y i)] [DecidablePred p] (f : ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i)) (x : ι) :
                                                                  (Homeomorph.symm (Homeomorph.piEquivPiSubtypeProd p Y)) f x = if h : p x then f.1 { val := x, property := h } else f.2 { val := x, property := h }
                                                                  def Homeomorph.piEquivPiSubtypeProd {ι : Type u_6} (p : ιProp) (Y : ιType u_7) [(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_symm_apply {ι : Type u_6} [DecidableEq ι] (i : ι) (Y : ιType u_7) [(j : ι) → TopologicalSpace (Y j)] (f : Y i × ((j : { j : ι // j i }) → Y j)) (j : ι) :
                                                                    (Homeomorph.symm (Homeomorph.piSplitAt i Y)) f j = if h : j = i then f.1 else f.2 { val := j, property := h }
                                                                    @[simp]
                                                                    theorem Homeomorph.piSplitAt_apply {ι : Type u_6} [DecidableEq ι] (i : ι) (Y : ιType u_7) [(j : ι) → TopologicalSpace (Y j)] (f : (j : ι) → Y j) :
                                                                    (Homeomorph.piSplitAt i Y) f = (f i, fun (j : { j : ι // ¬j = i }) => f j)
                                                                    def Homeomorph.piSplitAt {ι : Type u_6} [DecidableEq ι] (i : ι) (Y : ιType u_7) [(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_symm_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_6} [DecidableEq ι] (i : ι) (f : (fun (a : ι) => Y) i × ((j : { j : ι // j i }) → (fun (a : ι) => Y) j)) (j : ι) :
                                                                      (Homeomorph.symm (Homeomorph.funSplitAt Y i)) f j = if h : j = i then f.1 else f.2 { val := j, property := }
                                                                      @[simp]
                                                                      theorem Homeomorph.funSplitAt_apply (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_6} [DecidableEq ι] (i : ι) (f : (j : ι) → (fun (a : ι) => Y) j) :
                                                                      (Homeomorph.funSplitAt Y i) f = (f i, fun (j : { j : ι // ¬j = i }) => f j)
                                                                      def Homeomorph.funSplitAt (Y : Type u_2) [TopologicalSpace Y] {ι : Type u_6} [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) :
                                                                        (Equiv.toHomeomorph e 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
                                                                        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) :
                                                                          (Equiv.toHomeomorph e 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) :
                                                                          (Equiv.toHomeomorph e 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_4} [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) :
                                                                          @[simp]
                                                                          theorem Equiv.toHomeomorphOfInducing_toEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X Y) (hf : Inducing 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
                                                                          Instances For
                                                                            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
                                                                            Instances For