Documentation

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Topology and uniform structure of uniform convergence #

This files endows α → β with the topologies / uniform structures of

Since α → β is already endowed with the topologies and uniform structures of pointwise convergence, we introduce type aliases UniformFun α β (denoted α →ᵤ β) and UniformOnFun α β 𝔖 (denoted α →ᵤ[𝔖] β) and we actually endow these with the structures of uniform and 𝔖-convergence respectively.

Usual examples of the second construction include :

This file contains a lot of technical facts, so it is heavily commented, proofs included!

Main definitions #

Main statements #

Basic properties #

Functoriality and compatibility with product of uniform spaces #

In order to avoid the need for filter bases as much as possible when using these definitions, we develop an extensive API for manipulating these structures abstractly. As usual in the topology section of mathlib, we first state results about the complete lattices of UniformSpaces on fixed types, and then we use these to deduce categorical-like results about maps between two uniform spaces.

We only describe these in the harder case of 𝔖-convergence, as the names of the corresponding results for uniform convergence can easily be guessed.

Order statements #

An interesting note about these statements is that they are proved without ever unfolding the basis definition of the uniform structure of uniform convergence! Instead, we build a (not very interesting) Galois connection UniformFun.gc and then rely on the Galois connection API to do most of the work.

Morphism statements (unbundled) #

Isomorphism statements (bundled) #

Important use cases #

TODO #

References #

Tags #

uniform convergence

def UniformFun (α : Type u_1) (β : Type u_2) :
Type (max u_1 u_2)

The type of functions from α to β equipped with the uniform structure and topology of uniform convergence. We denote it α →ᵤ β.

Instances For
    def UniformOnFun (α : Type u_1) (β : Type u_2) :
    Set (Set α)Type (max u_1 u_2)

    The type of functions from α to β equipped with the uniform structure and topology of uniform convergence on some family 𝔖 of subsets of α. We denote it α →ᵤ[𝔖] β.

    Instances For
      instance instNonemptyUniformFun {α : Type u_1} {β : Type u_2} [Nonempty β] :
      instance instNonemptyUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Nonempty β] :
      Nonempty (UniformOnFun α β 𝔖)
      def UniformFun.ofFun {α : Type u_1} {β : Type u_2} :
      (αβ) UniformFun α β

      Reinterpret f : α → β as an element of α →ᵤ β.

      Instances For
        def UniformOnFun.ofFun {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) :
        (αβ) UniformOnFun α β 𝔖

        Reinterpret f : α → β as an element of α →ᵤ[𝔖] β.

        Instances For
          def UniformFun.toFun {α : Type u_1} {β : Type u_2} :
          UniformFun α β (αβ)

          Reinterpret f : α →ᵤ β as an element of α → β.

          Instances For
            def UniformOnFun.toFun {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) :
            UniformOnFun α β 𝔖 (αβ)

            Reinterpret f : α →ᵤ[𝔖] β as an element of α → β.

            Instances For
              def UniformFun.gen (α : Type u_1) (β : Type u_2) (V : Set (β × β)) :
              Set (UniformFun α β × UniformFun α β)

              Basis sets for the uniformity of uniform convergence: gen α β V is the set of pairs (f, g) of functions α →ᵤ β such that ∀ x, (f x, g x) ∈ V.

              Instances For
                theorem UniformFun.isBasis_gen (α : Type u_1) (β : Type u_2) (𝓑 : Filter (β × β)) :
                Filter.IsBasis (fun V => V 𝓑) (UniformFun.gen α β)

                If 𝓕 is a filter on β × β, then the set of all UniformFun.gen α β V for V ∈ 𝓕 is a filter basis on (α →ᵤ β) × (α →ᵤ β). This will only be applied to 𝓕 = 𝓤 β when β is equipped with a UniformSpace structure, but it is useful to define it for any filter in order to be able to state that it has a lower adjoint (see UniformFun.gc).

                def UniformFun.basis (α : Type u_1) (β : Type u_2) (𝓕 : Filter (β × β)) :

                For 𝓕 : Filter (β × β), this is the set of all UniformFun.gen α β V for V ∈ 𝓕 as a bundled FilterBasis over (α →ᵤ β) × (α →ᵤ β). This will only be applied to 𝓕 = 𝓤 β when β is equipped with a UniformSpace structure, but it is useful to define it for any filter in order to be able to state that it has a lower adjoint (see UniformFun.gc).

                Instances For
                  def UniformFun.filter (α : Type u_1) (β : Type u_2) (𝓕 : Filter (β × β)) :

                  For 𝓕 : Filter (β × β), this is the filter generated by the filter basis UniformFun.basis α β 𝓕. For 𝓕 = 𝓤 β, this will be the uniformity of uniform convergence on α.

                  Instances For
                    def UniformFun.phi (α : Type u_5) (β : Type u_6) (uvx : (UniformFun α β × UniformFun α β) × α) :
                    β × β
                    Instances For
                      theorem UniformFun.gc (α : Type u_1) (β : Type u_2) :
                      GaloisConnection (fun 𝓐 => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ )) fun 𝓕 => UniformFun.filter α β 𝓕

                      The function UniformFun.filter α β : Filter (β × β) → Filter ((α →ᵤ β) × (α →ᵤ β)) has a lower adjoint l (in the sense of GaloisConnection). The exact definition of l is not interesting; we will only use that it exists (in UniformFun.mono and UniformFun.iInf_eq) and that l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕) for each 𝓕 : Filter (γ × γ) and f : γ → α (in UniformFun.comap_eq).

                      Core of the uniform structure of uniform convergence.

                      Instances For
                        instance UniformFun.uniformSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] :

                        Uniform structure of uniform convergence, declared as an instance on α →ᵤ β. We will denote it 𝒰(α, β, uβ) in the rest of this file.

                        instance UniformFun.topologicalSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] :

                        Topology of uniform convergence, declared as an instance on α →ᵤ β.

                        theorem UniformFun.hasBasis_uniformity (α : Type u_1) (β : Type u_2) [UniformSpace β] :

                        By definition, the uniformity of α →ᵤ β admits the family {(f, g) | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓤 β as a filter basis.

                        theorem UniformFun.hasBasis_uniformity_of_basis (α : Type u_1) (β : Type u_2) [UniformSpace β] {ι : Sort u_5} {p : ιProp} {s : ιSet (β × β)} (h : Filter.HasBasis (uniformity β) p s) :

                        The uniformity of α →ᵤ β admits the family {(f, g) | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓑 as a filter basis, for any basis 𝓑 of 𝓤 β (in the case 𝓑 = (𝓤 β).as_basis this is true by definition).

                        theorem UniformFun.hasBasis_nhds_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (f : UniformFun α β) {p : ιProp} {s : ιSet (β × β)} (h : Filter.HasBasis (uniformity β) p s) :
                        Filter.HasBasis (nhds f) p fun i => {g | (f, g) UniformFun.gen α β (s i)}

                        For f : α →ᵤ β, 𝓝 f admits the family {g | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓑 as a filter basis, for any basis 𝓑 of 𝓤 β.

                        theorem UniformFun.hasBasis_nhds (α : Type u_1) (β : Type u_2) [UniformSpace β] (f : UniformFun α β) :
                        Filter.HasBasis (nhds f) (fun V => V uniformity β) fun V => {g | (f, g) UniformFun.gen α β V}

                        For f : α →ᵤ β, 𝓝 f admits the family {g | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓤 β as a filter basis.

                        theorem UniformFun.uniformContinuous_eval {α : Type u_1} (β : Type u_2) [UniformSpace β] (x : α) :
                        UniformContinuous (Function.eval x UniformFun.toFun)

                        Evaluation at a fixed point is uniformly continuous on α →ᵤ β.

                        theorem UniformFun.mono {α : Type u_1} {γ : Type u_3} :

                        If u₁ and u₂ are two uniform structures on γ and u₁ ≤ u₂, then 𝒰(α, γ, u₁) ≤ 𝒰(α, γ, u₂).

                        theorem UniformFun.iInf_eq {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {u : ιUniformSpace γ} :

                        If u is a family of uniform structures on γ, then 𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i).

                        theorem UniformFun.inf_eq {α : Type u_1} {γ : Type u_3} {u₁ : UniformSpace γ} {u₂ : UniformSpace γ} :

                        If u₁ and u₂ are two uniform structures on γ, then 𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂).

                        theorem UniformFun.comap_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {f : γβ} :

                        If u is a uniform structures on β and f : γ → β, then 𝒰(α, γ, comap f u) = comap (fun g ↦ f ∘ g) 𝒰(α, γ, u₁).

                        theorem UniformFun.postcomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] {f : γβ} (hf : UniformContinuous f) :
                        UniformContinuous (UniformFun.ofFun (fun x => f x) UniformFun.toFun)

                        Post-composition by a uniformly continuous function is uniformly continuous on α →ᵤ β.

                        More precisely, if f : γ → β is uniformly continuous, then (fun g ↦ f ∘ g) : (α →ᵤ γ) → (α →ᵤ β) is uniformly continuous.

                        theorem UniformFun.postcomp_uniformInducing {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] {f : γβ} (hf : UniformInducing f) :
                        UniformInducing (UniformFun.ofFun (fun x => f x) UniformFun.toFun)

                        Post-composition by a uniform inducing is a uniform inducing for the uniform structures of uniform convergence.

                        More precisely, if f : γ → β is a uniform inducing, then (λ g, f ∘ g) : (α →ᵤ γ) → (α →ᵤ β) is a uniform inducing.

                        def UniformFun.congrRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] (e : γ ≃ᵤ β) :

                        Turn a uniform isomorphism γ ≃ᵤ β into a uniform isomorphism (α →ᵤ γ) ≃ᵤ (α →ᵤ β) by post-composing.

                        Instances For
                          theorem UniformFun.precomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {f : γα} :
                          UniformContinuous fun g => UniformFun.ofFun (g f)

                          Pre-composition by any function is uniformly continuous for the uniform structures of uniform convergence.

                          More precisely, for any f : γ → α, the function (λ g, g ∘ f) : (α →ᵤ β) → (γ →ᵤ β) is uniformly continuous.

                          def UniformFun.congrLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] (e : γ α) :

                          Turn a bijection γ ≃ α into a uniform isomorphism (γ →ᵤ β) ≃ᵤ (α →ᵤ β) by pre-composing.

                          Instances For

                            The topology of uniform convergence is T₂.

                            theorem UniformFun.uniformContinuous_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] :
                            UniformContinuous UniformFun.toFun

                            The natural map UniformFun.toFun from α →ᵤ β to α → β is uniformly continuous.

                            In other words, the uniform structure of uniform convergence is finer than that of pointwise convergence, aka the product uniform structure.

                            theorem UniformFun.tendsto_iff_tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [UniformSpace β] {F : ιUniformFun α β} {f : UniformFun α β} :

                            The topology of uniform convergence indeed gives the same notion of convergence as TendstoUniformly.

                            def UniformFun.uniformEquivProdArrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] :
                            UniformFun α (β × γ) ≃ᵤ UniformFun α β × UniformFun α γ

                            The natural bijection between α → β × γ and (α → β) × (α → γ), upgraded to a uniform isomorphism between α →ᵤ β × γ and (α →ᵤ β) × (α →ᵤ γ).

                            Instances For
                              def UniformFun.uniformEquivPiComm (α : Type u_1) {ι : Type u_4} (δ : ιType u_5) [(i : ι) → UniformSpace (δ i)] :
                              UniformFun α ((i : ι) → δ i) ≃ᵤ ((i : ι) → UniformFun α (δ i))

                              The natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform isomorphism between α →ᵤ (Π i, δ i) and Π i, α →ᵤ δ i.

                              Instances For
                                def UniformOnFun.gen {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (S : Set α) (V : Set (β × β)) :
                                Set (UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖)

                                Basis sets for the uniformity of 𝔖-convergence: for S : Set α and V : Set (β × β), gen 𝔖 S V is the set of pairs (f, g) of functions α →ᵤ[𝔖] β such that ∀ x ∈ S, (f x, g x) ∈ V. Note that the family 𝔖 : Set (Set α) is only used to specify which type alias of α → β to use here.

                                Instances For
                                  theorem UniformOnFun.gen_eq_preimage_restrict {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (S : Set α) (V : Set (β × β)) :
                                  UniformOnFun.gen 𝔖 S V = Prod.map (Set.restrict S UniformFun.toFun) (Set.restrict S UniformFun.toFun) ⁻¹' UniformFun.gen (S) β V

                                  For S : Set α and V : Set (β × β), we have UniformOnFun.gen 𝔖 S V = (S.restrict × S.restrict) ⁻¹' (UniformFun.gen S β V). This is the crucial fact for proving that the family UniformOnFun.gen S V for S ∈ 𝔖 and V ∈ 𝓤 β is indeed a basis for the uniformity α →ᵤ[𝔖] β endowed with 𝒱(α, β, 𝔖, uβ) the uniform structure of 𝔖-convergence, as defined in uniform_on_fun.uniform_space.

                                  theorem UniformOnFun.gen_mono {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {S : Set α} {S' : Set α} {V : Set (β × β)} {V' : Set (β × β)} (hS : S' S) (hV : V V') :

                                  UniformOnFun.gen is antitone in the first argument and monotone in the second.

                                  theorem UniformOnFun.isBasis_gen {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (h : Set.Nonempty 𝔖) (h' : DirectedOn (fun x x_1 => x x_1) 𝔖) (𝓑 : FilterBasis (β × β)) :
                                  Filter.IsBasis (fun SV => SV.fst 𝔖 SV.snd 𝓑) fun SV => UniformOnFun.gen 𝔖 SV.fst SV.snd

                                  If 𝔖 : Set (Set α) is nonempty and directed and 𝓑 is a filter basis on β × β, then the family UniformOnFun.gen 𝔖 S V for S ∈ 𝔖 and V ∈ 𝓑 is a filter basis on (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β). We will show in has_basis_uniformity_of_basis that, if 𝓑 is a basis for 𝓤 β, then the corresponding filter is the uniformity of α →ᵤ[𝔖] β.

                                  instance UniformOnFun.uniformSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :

                                  Uniform structure of 𝔖-convergence, i.e uniform convergence on the elements of 𝔖, declared as an instance on α →ᵤ[𝔖] β. It is defined as the infimum, for S ∈ 𝔖, of the pullback by S.restrict, the map of restriction to S, of the uniform structure 𝒰(s, β, uβ) on ↥S →ᵤ β. We will denote it 𝒱(α, β, 𝔖, uβ), where is the uniform structure on β.

                                  instance UniformOnFun.topologicalSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :

                                  Topology of 𝔖-convergence, i.e uniform convergence on the elements of 𝔖, declared as an instance on α →ᵤ[𝔖] β.

                                  theorem UniformOnFun.topologicalSpace_eq (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
                                  UniformOnFun.topologicalSpace α β 𝔖 = ⨅ (s : Set α) (_ : s 𝔖), TopologicalSpace.induced (Set.restrict s UniformFun.toFun) (UniformFun.topologicalSpace (s) β)

                                  The topology of 𝔖-convergence is the infimum, for S ∈ 𝔖, of topology induced by the map of S.restrict : (α →ᵤ[𝔖] β) → (↥S →ᵤ β) of restriction to S, where ↥S →ᵤ β is endowed with the topology of uniform convergence.

                                  theorem UniformOnFun.hasBasis_uniformity_of_basis_aux₁ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) {p : ιProp} {s : ιSet (β × β)} (hb : Filter.HasBasis (uniformity β) p s) (S : Set α) :
                                  Filter.HasBasis (uniformity (UniformOnFun α β 𝔖)) p fun i => UniformOnFun.gen 𝔖 S (s i)
                                  theorem UniformOnFun.hasBasis_uniformity_of_basis_aux₂ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (h : DirectedOn (fun x x_1 => x x_1) 𝔖) {p : ιProp} {s : ιSet (β × β)} (hb : Filter.HasBasis (uniformity β) p s) :
                                  theorem UniformOnFun.hasBasis_uniformity_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (h : Set.Nonempty 𝔖) (h' : DirectedOn (fun x x_1 => x x_1) 𝔖) {p : ιProp} {s : ιSet (β × β)} (hb : Filter.HasBasis (uniformity β) p s) :
                                  Filter.HasBasis (uniformity (UniformOnFun α β 𝔖)) (fun Si => Si.fst 𝔖 p Si.snd) fun Si => UniformOnFun.gen 𝔖 Si.fst (s Si.snd)

                                  If 𝔖 : Set (Set α) is nonempty and directed and 𝓑 is a filter basis of 𝓤 β, then the uniformity of α →ᵤ[𝔖] β admits the family {(f, g) | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓑 as a filter basis.

                                  theorem UniformOnFun.hasBasis_uniformity (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (h : Set.Nonempty 𝔖) (h' : DirectedOn (fun x x_1 => x x_1) 𝔖) :
                                  Filter.HasBasis (uniformity (UniformOnFun α β 𝔖)) (fun SV => SV.fst 𝔖 SV.snd uniformity β) fun SV => UniformOnFun.gen 𝔖 SV.fst SV.snd

                                  If 𝔖 : Set (Set α) is nonempty and directed, then the uniformity of α →ᵤ[𝔖] β admits the family {(f, g) | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓤 β as a filter basis.

                                  theorem UniformOnFun.hasBasis_nhds_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (h : Set.Nonempty 𝔖) (h' : DirectedOn (fun x x_1 => x x_1) 𝔖) {p : ιProp} {s : ιSet (β × β)} (hb : Filter.HasBasis (uniformity β) p s) :
                                  Filter.HasBasis (nhds f) (fun Si => Si.fst 𝔖 p Si.snd) fun Si => {g | (g, f) UniformOnFun.gen 𝔖 Si.fst (s Si.snd)}

                                  For f : α →ᵤ[𝔖] β, where 𝔖 : Set (Set α) is nonempty and directed, 𝓝 f admits the family {g | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓑 as a filter basis, for any basis 𝓑 of 𝓤 β.

                                  theorem UniformOnFun.hasBasis_nhds (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (h : Set.Nonempty 𝔖) (h' : DirectedOn (fun x x_1 => x x_1) 𝔖) :
                                  Filter.HasBasis (nhds f) (fun SV => SV.fst 𝔖 SV.snd uniformity β) fun SV => {g | (g, f) UniformOnFun.gen 𝔖 SV.fst SV.snd}

                                  For f : α →ᵤ[𝔖] β, where 𝔖 : Set (Set α) is nonempty and directed, 𝓝 f admits the family {g | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓤 β as a filter basis.

                                  theorem UniformOnFun.uniformContinuous_restrict (α : Type u_1) (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (h : s 𝔖) :
                                  UniformContinuous (UniformFun.ofFun Set.restrict s ↑(UniformOnFun.toFun 𝔖))

                                  If S ∈ 𝔖, then the restriction to S is a uniformly continuous map from α →ᵤ[𝔖] β to ↥S →ᵤ β.

                                  theorem UniformOnFun.mono {α : Type u_1} {γ : Type u_3} ⦃u₁ : UniformSpace γ ⦃u₂ : UniformSpace γ (hu : u₁ u₂) ⦃𝔖₁ : Set (Set α) ⦃𝔖₂ : Set (Set α) (h𝔖 : 𝔖₂ 𝔖₁) :

                                  Let u₁, u₂ be two uniform structures on γ and 𝔖₁ 𝔖₂ : Set (Set α). If u₁ ≤ u₂ and 𝔖₂ ⊆ 𝔖₁ then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).

                                  theorem UniformOnFun.uniformContinuous_eval_of_mem {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) {x : α} (hxs : x s) (hs : s 𝔖) :

                                  If x : α is in some S ∈ 𝔖, then evaluation at x is uniformly continuous on α →ᵤ[𝔖] β.

                                  theorem UniformOnFun.iInf_eq {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : Set (Set α)} {u : ιUniformSpace γ} :
                                  UniformOnFun.uniformSpace α γ 𝔖 = ⨅ (i : ι), UniformOnFun.uniformSpace α γ 𝔖

                                  If u is a family of uniform structures on γ, then 𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).

                                  theorem UniformOnFun.inf_eq {α : Type u_1} {γ : Type u_3} {𝔖 : Set (Set α)} {u₁ : UniformSpace γ} {u₂ : UniformSpace γ} :

                                  If u₁ and u₂ are two uniform structures on γ, then 𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂).

                                  theorem UniformOnFun.comap_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {f : γβ} :
                                  UniformOnFun.uniformSpace α γ 𝔖 = UniformSpace.comap ((fun x x_1 => x x_1) f) (UniformOnFun.uniformSpace α β 𝔖)

                                  If u is a uniform structure on β and f : γ → β, then 𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁).

                                  theorem UniformOnFun.postcomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γβ} (hf : UniformContinuous f) :
                                  UniformContinuous (↑(UniformOnFun.ofFun 𝔖) (fun x x_1 => x x_1) f ↑(UniformOnFun.toFun 𝔖))

                                  Post-composition by a uniformly continuous function is uniformly continuous for the uniform structures of 𝔖-convergence.

                                  More precisely, if f : γ → β is uniformly continuous, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is uniformly continuous.

                                  theorem UniformOnFun.postcomp_uniformInducing {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γβ} (hf : UniformInducing f) :
                                  UniformInducing (↑(UniformOnFun.ofFun 𝔖) (fun x x_1 => x x_1) f ↑(UniformOnFun.toFun 𝔖))

                                  Post-composition by a uniform inducing is a uniform inducing for the uniform structures of 𝔖-convergence.

                                  More precisely, if f : γ → β is a uniform inducing, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is a uniform inducing.

                                  def UniformOnFun.congrRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] (e : γ ≃ᵤ β) :
                                  UniformOnFun α γ 𝔖 ≃ᵤ UniformOnFun α β 𝔖

                                  Turn a uniform isomorphism γ ≃ᵤ β into a uniform isomorphism (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β) by post-composing.

                                  Instances For
                                    theorem UniformOnFun.precomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} {f : γα} (hf : 𝔗 Set.image f ⁻¹' 𝔖) :
                                    UniformContinuous fun g => ↑(UniformOnFun.ofFun 𝔗) (g f)

                                    Let f : γ → α, 𝔖 : Set (Set α), 𝔗 : Set (Set γ), and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖. Then, the function (fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β) is uniformly continuous.

                                    Note that one can easily see that assuming ∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f '' T ⊆ S would work too, but we will get this for free when we prove that 𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ) where 𝔖' is the noncovering bornology generated by 𝔖.

                                    def UniformOnFun.congrLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} (e : γ α) (he : 𝔗 Set.image e ⁻¹' 𝔖) (he' : 𝔖 Set.preimage e ⁻¹' 𝔗) :
                                    UniformOnFun γ β 𝔗 ≃ᵤ UniformOnFun α β 𝔖

                                    Turn a bijection e : γ ≃ α such that we have both ∀ T ∈ 𝔗, e '' T ∈ 𝔖 and ∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗 into a uniform isomorphism (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β) by pre-composing.

                                    Instances For
                                      theorem UniformOnFun.t2Space_of_covering {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [T2Space β] (h : ⋃₀ 𝔖 = Set.univ) :
                                      T2Space (UniformOnFun α β 𝔖)

                                      If 𝔖 covers α, then the topology of 𝔖-convergence is T₂.

                                      theorem UniformOnFun.uniformContinuous_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} (h : ⋃₀ 𝔖 = Set.univ) :

                                      If 𝔖 covers α, the natural map UniformOnFun.toFun from α →ᵤ[𝔖] β to α → β is uniformly continuous.

                                      In other words, if 𝔖 covers α, then the uniform structure of 𝔖-convergence is finer than that of pointwise convergence.

                                      theorem UniformOnFun.tendsto_iff_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [UniformSpace β] {𝔖 : Set (Set α)} {F : ιUniformOnFun α β 𝔖} {f : UniformOnFun α β 𝔖} :
                                      Filter.Tendsto F p (nhds f) ∀ (s : Set α), s 𝔖TendstoUniformlyOn F f p s

                                      Convergence in the topology of 𝔖-convergence means uniform convergence on S (in the sense of TendstoUniformlyOn) for all S ∈ 𝔖.

                                      def UniformOnFun.uniformEquivProdArrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] :
                                      UniformOnFun α (β × γ) 𝔖 ≃ᵤ UniformOnFun α β 𝔖 × UniformOnFun α γ 𝔖

                                      The natural bijection between α → β × γ and (α → β) × (α → γ), upgraded to a uniform isomorphism between α →ᵤ[𝔖] β × γ and (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ).

                                      Instances For
                                        def UniformOnFun.uniformEquivPiComm {α : Type u_1} {ι : Type u_4} (𝔖 : Set (Set α)) (δ : ιType u_5) [(i : ι) → UniformSpace (δ i)] :
                                        UniformOnFun α ((i : ι) → δ i) 𝔖 ≃ᵤ ((i : ι) → UniformOnFun α (δ i) 𝔖)

                                        The natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform isomorphism between α →ᵤ[𝔖] (Π i, δ i) and Π i, α →ᵤ[𝔖] δ i.

                                        Instances For