Documentation

Mathlib.Topology.UniformSpace.Equiv

Uniform isomorphisms #

This file defines uniform isomorphisms between two uniform spaces. They are bijections with both directions uniformly continuous. We denote uniform isomorphisms with the notation ≃ᵤ.

Main definitions #

structure UniformEquiv (α : Type u_4) (β : Type u_5) [UniformSpace α] [UniformSpace β] extends Equiv :
Type (max u_4 u_5)

Uniform isomorphism between α and β

Instances For

    Uniform isomorphism between α and β

    Equations
    Instances For
      theorem UniformEquiv.toEquiv_injective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] :
      Function.Injective UniformEquiv.toEquiv
      instance UniformEquiv.instEquivLikeUniformEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] :
      EquivLike (α ≃ᵤ β) α β
      Equations
      • UniformEquiv.instEquivLikeUniformEquiv = { coe := fun (h : α ≃ᵤ β) => h.toEquiv, inv := fun (h : α ≃ᵤ β) => h.symm, left_inv := , right_inv := , coe_injective' := }
      @[simp]
      theorem UniformEquiv.uniformEquiv_mk_coe {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (a : α β) (b : UniformContinuous a.toFun) (c : UniformContinuous a.invFun) :
      { toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c } = a
      def UniformEquiv.symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
      β ≃ᵤ α

      Inverse of a uniform isomorphism.

      Equations
      • UniformEquiv.symm h = { toEquiv := h.symm, uniformContinuous_toFun := , uniformContinuous_invFun := }
      Instances For
        def UniformEquiv.Simps.apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
        αβ

        See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

        Equations
        Instances For
          def UniformEquiv.Simps.symm_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
          βα

          See Note [custom simps projection]

          Equations
          Instances For
            @[simp]
            theorem UniformEquiv.coe_toEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
            h.toEquiv = h
            @[simp]
            theorem UniformEquiv.coe_symm_toEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
            h.symm = (UniformEquiv.symm h)
            theorem UniformEquiv.ext {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] {h : α ≃ᵤ β} {h' : α ≃ᵤ β} (H : ∀ (x : α), h x = h' x) :
            h = h'
            @[simp]
            theorem UniformEquiv.refl_apply (α : Type u_4) [UniformSpace α] :
            (UniformEquiv.refl α) = id
            def UniformEquiv.refl (α : Type u_4) [UniformSpace α] :
            α ≃ᵤ α

            Identity map as a uniform isomorphism.

            Equations
            Instances For
              def UniformEquiv.trans {α : Type u} {β : Type u_1} {γ : Type u_2} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) :
              α ≃ᵤ γ

              Composition of two uniform isomorphisms.

              Equations
              • UniformEquiv.trans h₁ h₂ = { toEquiv := h₁.trans h₂.toEquiv, uniformContinuous_toFun := , uniformContinuous_invFun := }
              Instances For
                @[simp]
                theorem UniformEquiv.trans_apply {α : Type u} {β : Type u_1} {γ : Type u_2} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α) :
                (UniformEquiv.trans h₁ h₂) a = h₂ (h₁ a)
                @[simp]
                theorem UniformEquiv.uniformEquiv_mk_coe_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (a : α β) (b : UniformContinuous a.toFun) (c : UniformContinuous a.invFun) :
                (UniformEquiv.symm { toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c }) = a.symm
                theorem UniformEquiv.uniformContinuous {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                theorem UniformEquiv.continuous {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                def UniformEquiv.toHomeomorph {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) :
                α ≃ₜ β

                A uniform isomorphism as a homeomorphism.

                Equations
                Instances For
                  theorem UniformEquiv.toHomeomorph_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) :
                  @[simp]
                  theorem UniformEquiv.apply_symm_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (x : β) :
                  h ((UniformEquiv.symm h) x) = x
                  @[simp]
                  theorem UniformEquiv.symm_apply_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (x : α) :
                  (UniformEquiv.symm h) (h x) = x
                  theorem UniformEquiv.bijective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                  theorem UniformEquiv.injective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                  theorem UniformEquiv.surjective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                  def UniformEquiv.changeInv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (f : α ≃ᵤ β) (g : βα) (hg : Function.RightInverse g f) :
                  α ≃ᵤ β

                  Change the uniform equiv f to make the inverse function definitionally equal to g.

                  Equations
                  • UniformEquiv.changeInv f g hg = let_fun this := ; { toEquiv := { toFun := f, invFun := g, left_inv := , right_inv := }, uniformContinuous_toFun := , uniformContinuous_invFun := }
                  Instances For
                    @[simp]
                    theorem UniformEquiv.symm_comp_self {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                    (UniformEquiv.symm h) h = id
                    @[simp]
                    theorem UniformEquiv.self_comp_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                    h (UniformEquiv.symm h) = id
                    theorem UniformEquiv.range_coe {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                    Set.range h = Set.univ
                    theorem UniformEquiv.image_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                    theorem UniformEquiv.image_preimage {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (s : Set β) :
                    h '' (h ⁻¹' s) = s
                    theorem UniformEquiv.preimage_image {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (s : Set α) :
                    h ⁻¹' (h '' s) = s
                    theorem UniformEquiv.uniformInducing {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                    theorem UniformEquiv.comap_eq {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                    UniformSpace.comap (h) inst✝ = inst✝¹
                    theorem UniformEquiv.uniformEmbedding {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
                    noncomputable def UniformEquiv.ofUniformEmbedding {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (f : αβ) (hf : UniformEmbedding f) :
                    α ≃ᵤ (Set.range f)

                    Uniform equiv given a uniform embedding.

                    Equations
                    Instances For
                      def UniformEquiv.setCongr {α : Type u} [UniformSpace α] {s : Set α} {t : Set α} (h : s = t) :
                      s ≃ᵤ t

                      If two sets are equal, then they are uniformly equivalent.

                      Equations
                      Instances For
                        def UniformEquiv.prodCongr {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
                        α × γ ≃ᵤ β × δ

                        Product of two uniform isomorphisms.

                        Equations
                        Instances For
                          @[simp]
                          theorem UniformEquiv.prodCongr_symm {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
                          @[simp]
                          theorem UniformEquiv.coe_prodCongr {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
                          (UniformEquiv.prodCongr h₁ h₂) = Prod.map h₁ h₂
                          def UniformEquiv.prodComm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] :
                          α × β ≃ᵤ β × α

                          α × β is uniformly isomorphic to β × α.

                          Equations
                          Instances For
                            @[simp]
                            theorem UniformEquiv.coe_prodComm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] :
                            (UniformEquiv.prodComm α β) = Prod.swap
                            def UniformEquiv.prodAssoc (α : Type u) (β : Type u_1) (γ : Type u_2) [UniformSpace α] [UniformSpace β] [UniformSpace γ] :
                            (α × β) × γ ≃ᵤ α × β × γ

                            (α × β) × γ is uniformly isomorphic to α × (β × γ).

                            Equations
                            Instances For
                              @[simp]
                              theorem UniformEquiv.prodPunit_apply (α : Type u) [UniformSpace α] :
                              (UniformEquiv.prodPunit α) = fun (p : α × PUnit.{u_4 + 1} ) => p.1

                              α × {*} is uniformly isomorphic to α.

                              Equations
                              Instances For
                                @[simp]
                                theorem UniformEquiv.coe_punitProd (α : Type u) [UniformSpace α] :
                                (UniformEquiv.punitProd α) = Prod.snd
                                @[simp]
                                theorem UniformEquiv.piCongrLeft_apply {ι : Type u_4} {ι' : Type u_5} {β : ι'Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ι') :
                                ∀ (a : (b : ι) → β (e.symm.symm b)) (a_1 : ι'), (UniformEquiv.piCongrLeft e) a a_1 = (Equiv.piCongrLeft' β e.symm).symm a a_1
                                @[simp]
                                theorem UniformEquiv.piCongrLeft_toEquiv {ι : Type u_4} {ι' : Type u_5} {β : ι'Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ι') :
                                def UniformEquiv.piCongrLeft {ι : Type u_4} {ι' : Type u_5} {β : ι'Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ι') :
                                ((i : ι) → β (e i)) ≃ᵤ ((j : ι') → β j)

                                Equiv.piCongrLeft as a uniform isomorphism: this is the natural isomorphism Π i, β (e i) ≃ᵤ Π j, β j obtained from a bijection ι ≃ ι'.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem UniformEquiv.piCongrRight_apply {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) (H : (a : ι) → (fun (i : ι) => β₁ i) a) (a : ι) :
                                  (UniformEquiv.piCongrRight F) H a = (F a) (H a)
                                  @[simp]
                                  theorem UniformEquiv.piCongrRight_toEquiv {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
                                  (UniformEquiv.piCongrRight F).toEquiv = Equiv.piCongrRight fun (i : ι) => (F i).toEquiv
                                  def UniformEquiv.piCongrRight {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
                                  ((i : ι) → β₁ i) ≃ᵤ ((i : ι) → β₂ i)

                                  Equiv.piCongrRight as a uniform isomorphism: this is the natural isomorphism Π i, β₁ i ≃ᵤ Π j, β₂ i obtained from uniform isomorphisms β₁ i ≃ᵤ β₂ i for each i.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem UniformEquiv.piCongrRight_symm {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
                                    @[simp]
                                    theorem UniformEquiv.piCongr_toEquiv {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁Type u_6} {β₂ : ι₂Type u_7} [(i₁ : ι₁) → UniformSpace (β₁ i₁)] [(i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) :
                                    (UniformEquiv.piCongr e F).toEquiv = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv).trans (Equiv.piCongrLeft β₂ e)
                                    @[simp]
                                    theorem UniformEquiv.piCongr_apply {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁Type u_6} {β₂ : ι₂Type u_7} [(i₁ : ι₁) → UniformSpace (β₁ i₁)] [(i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) :
                                    ∀ (a : (i : ι₁) → β₁ i) (i₂ : ι₂), (UniformEquiv.piCongr e F) a i₂ = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv) a (e.symm i₂)
                                    def UniformEquiv.piCongr {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁Type u_6} {β₂ : ι₂Type u_7} [(i₁ : ι₁) → UniformSpace (β₁ i₁)] [(i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) :
                                    ((i₁ : ι₁) → β₁ i₁) ≃ᵤ ((i₂ : ι₂) → β₂ i₂)

                                    Equiv.piCongr as a uniform isomorphism: this is the natural isomorphism Π i₁, β₁ i ≃ᵤ Π i₂, β₂ i₂ obtained from a bijection ι₁ ≃ ι₂ and isomorphisms β₁ i₁ ≃ᵤ β₂ (e i₁) for each i₁ : ι₁.

                                    Equations
                                    Instances For

                                      Uniform equivalence between ULift α and α.

                                      Equations
                                      • UniformEquiv.ulift α = let __src := Equiv.ulift; { toEquiv := __src, uniformContinuous_toFun := , uniformContinuous_invFun := }
                                      Instances For
                                        @[simp]
                                        theorem UniformEquiv.funUnique_apply (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] :
                                        (UniformEquiv.funUnique ι α) = fun (f : ια) => f default
                                        @[simp]
                                        theorem UniformEquiv.funUnique_symm_apply (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] :
                                        def UniformEquiv.funUnique (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] :
                                        (ια) ≃ᵤ α

                                        If ι has a unique element, then ι → α is uniformly isomorphic to α.

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

                                          Uniform isomorphism between dependent functions Π i : Fin 2, α i and α 0 × α 1.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem UniformEquiv.finTwoArrow_symm_apply (α : Type u_4) [UniformSpace α] :
                                            (UniformEquiv.symm (UniformEquiv.finTwoArrow α)) = fun (x : α × α) => ![x.1, x.2]
                                            @[simp]
                                            theorem UniformEquiv.finTwoArrow_apply (α : Type u_4) [UniformSpace α] :
                                            (UniformEquiv.finTwoArrow α) = fun (f : Fin 2α) => (f 0, f 1)
                                            def UniformEquiv.finTwoArrow (α : Type u_4) [UniformSpace α] :
                                            (Fin 2α) ≃ᵤ α × α

                                            Uniform isomorphism between α² = Fin 2 → α and α × α.

                                            Equations
                                            Instances For
                                              def UniformEquiv.image {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) (s : Set α) :
                                              s ≃ᵤ (e '' s)

                                              A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.

                                              Equations
                                              Instances For
                                                def Equiv.toUniformEquivOfUniformInducing {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (f : α β) (hf : UniformInducing f) :
                                                α ≃ᵤ β

                                                A uniform inducing equiv between uniform spaces is a uniform isomorphism.

                                                Equations
                                                Instances For