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 α →ᵤ β.

Equations
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 α →ᵤ[𝔖] β.

    Equations
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        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 α →ᵤ[𝔖] β.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          instance instNonemptyUniformFun {α : Type u_1} {β : Type u_2} [Nonempty β] :
          Equations
          • =
          instance instNonemptyUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Nonempty β] :
          Nonempty (UniformOnFun α β 𝔖)
          Equations
          • =
          instance instSubsingletonUniformFun {α : Type u_1} {β : Type u_2} [Subsingleton β] :
          Equations
          • =
          instance instSubsingletonUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Subsingleton β] :
          Equations
          • =
          def UniformFun.ofFun {α : Type u_1} {β : Type u_2} :
          (αβ) UniformFun α β

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

          Equations
          • UniformFun.ofFun = { toFun := fun (x : αβ) => x, invFun := fun (x : UniformFun α β) => x, left_inv := , right_inv := }
          Instances For
            def UniformOnFun.ofFun {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) :
            (αβ) UniformOnFun α β 𝔖

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

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

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

              Equations
              • UniformFun.toFun = UniformFun.ofFun.symm
              Instances For
                def UniformOnFun.toFun {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) :
                UniformOnFun α β 𝔖 (αβ)

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

                Equations
                Instances For
                  @[simp]
                  theorem UniformFun.toFun_ofFun {α : Type u_1} {β : Type u_2} (f : αβ) :
                  UniformFun.toFun (UniformFun.ofFun f) = f
                  @[simp]
                  theorem UniformFun.ofFun_toFun {α : Type u_1} {β : Type u_2} (f : UniformFun α β) :
                  UniformFun.ofFun (UniformFun.toFun f) = f
                  @[simp]
                  theorem UniformOnFun.toFun_ofFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : αβ) :
                  @[simp]
                  theorem UniformOnFun.ofFun_toFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : UniformOnFun α β 𝔖) :
                  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.

                  Equations
                  Instances For
                    theorem UniformFun.isBasis_gen (α : Type u_1) (β : Type u_2) (𝓑 : Filter (β × β)) :
                    Filter.IsBasis (fun (V : Set (β × β)) => 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).

                    Equations
                    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 α.

                      Equations
                      Instances For
                        def UniformFun.phi (α : Type u_5) (β : Type u_6) (uvx : (UniformFun α β × UniformFun α β) × α) :
                        β × β
                        Equations
                        Instances For
                          theorem UniformFun.gc (α : Type u_1) (β : Type u_2) :
                          GaloisConnection (fun (𝓐 : Filter (UniformFun α β × UniformFun α β)) => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ )) fun (𝓕 : Filter (β × β)) => 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.

                          Equations
                          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.

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

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

                            Equations
                            theorem UniformFun.hasBasis_uniformity (α : Type u_1) (β : Type u_2) [UniformSpace β] :
                            (uniformity (UniformFun α β)).HasBasis (fun (x : Set (β × β)) => x uniformity β) (UniformFun.gen α β)

                            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 : (uniformity β).HasBasis p s) :
                            (uniformity (UniformFun α β)).HasBasis p (UniformFun.gen α β 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 : (uniformity β).HasBasis p s) :
                            (nhds f).HasBasis p fun (i : ι) => {g : UniformFun α β | (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 α β) :
                            (nhds f).HasBasis (fun (V : Set (β × β)) => V uniformity β) fun (V : Set (β × β)) => {g : UniformFun α β | (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 α →ᵤ β.

                            @[simp]
                            theorem UniformFun.mem_gen {α : Type u_1} {β : Type u_2} {f : UniformFun α β} {g : UniformFun α β} {V : Set (β × β)} :
                            (f, g) UniformFun.gen α β V ∀ (x : α), (UniformFun.toFun f x, UniformFun.toFun g x) V
                            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.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 function is a uniform inducing function for the uniform structures of uniform convergence.

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

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

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

                            More precisely, if f : γ → β is a uniform embedding, then (f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β) is a uniform embedding.

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

                            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.

                            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.

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

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

                              More precisely, for any f : γ → α, the function (· ∘ 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.

                              Equations
                              Instances For
                                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.

                                instance UniformFun.instT2Space {α : Type u_1} {β : Type u_2} [UniformSpace β] [T2Space β] :

                                The topology of uniform convergence is T₂.

                                Equations
                                • =
                                theorem UniformFun.tendsto_iff_tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [UniformSpace β] {F : ιUniformFun α β} {f : UniformFun α β} :
                                Filter.Tendsto F p (nhds f) TendstoUniformly (UniformFun.toFun F) (UniformFun.toFun f) p

                                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 (α →ᵤ β) × (α →ᵤ γ).

                                Equations
                                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.

                                  Equations
                                  Instances For
                                    theorem UniformFun.isClosed_setOf_continuous (α : Type u_1) {β : Type u_2} [UniformSpace β] [TopologicalSpace α] :
                                    IsClosed {f : UniformFun α β | Continuous (UniformFun.toFun f)}

                                    The set of continuous functions is closed in the uniform convergence topology. This is a simple wrapper over TendstoUniformly.continuous.

                                    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.

                                    Equations
                                    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 (S.restrict UniformFun.toFun) (S.restrict 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 UniformOnFun.uniformSpace.

                                      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 : 𝔖.Nonempty) (h' : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) (𝓑 : FilterBasis (β × β)) :
                                      Filter.IsBasis (fun (SV : Set α × Set (β × β)) => SV.1 𝔖 SV.2 𝓑) fun (SV : Set α × Set (β × β)) => UniformOnFun.gen 𝔖 SV.1 SV.2

                                      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 β.

                                      Equations
                                      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 α →ᵤ[𝔖] β.

                                      Equations
                                      theorem UniformOnFun.topologicalSpace_eq (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
                                      UniformOnFun.topologicalSpace α β 𝔖 = s𝔖, TopologicalSpace.induced (UniformFun.ofFun s.restrict (UniformOnFun.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 : (uniformity β).HasBasis p s) (S : Set α) :
                                      (uniformity (UniformOnFun α β 𝔖)).HasBasis 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 : Set α) => x x_1) 𝔖) {p : ιProp} {s : ιSet (β × β)} (hb : (uniformity β).HasBasis p s) :
                                      DirectedOn ((fun (s : Set α) => UniformSpace.comap s.restrict (UniformFun.uniformSpace (s) β)) ⁻¹'o GE.ge) 𝔖
                                      theorem UniformOnFun.hasBasis_uniformity_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) {p : ιProp} {s : ιSet (β × β)} (hb : (uniformity β).HasBasis p s) :
                                      (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun (Si : Set α × ι) => Si.1 𝔖 p Si.2) fun (Si : Set α × ι) => UniformOnFun.gen 𝔖 Si.1 (s Si.2)

                                      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 : 𝔖.Nonempty) (h' : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) :
                                      (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun (SV : Set α × Set (β × β)) => SV.1 𝔖 SV.2 uniformity β) fun (SV : Set α × Set (β × β)) => UniformOnFun.gen 𝔖 SV.1 SV.2

                                      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_uniformity_of_covering_of_basis {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} {ι' : Type u_6} [Nonempty ι] {t : ιSet α} {p : ι'Prop} {V : ι'Set (β × β)} (ht : ∀ (i : ι), t i 𝔖) (hdir : Directed (fun (x x_1 : Set α) => x x_1) t) (hex : s𝔖, ∃ (i : ι), s t i) (hb : (uniformity β).HasBasis p V) :
                                      (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun (i : ι × ι') => p i.2) fun (i : ι × ι') => UniformOnFun.gen 𝔖 (t i.1) (V i.2)

                                      Let t i be a nonempty directed subfamily of 𝔖 such that every s ∈ 𝔖 is included in some t i. Let V bounded by p be a basis of entourages of β.

                                      Then UniformOnFun.gen 𝔖 (t i) (V j) bounded by p j is a basis of entourages of α →ᵤ[𝔖] β.

                                      theorem UniformOnFun.hasAntitoneBasis_uniformity {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} [Preorder ι] [IsDirected ι fun (x x_1 : ι) => x x_1] {t : ιSet α} {V : ιSet (β × β)} (ht : ∀ (n : ι), t n 𝔖) (hmono : Monotone t) (hex : s𝔖, ∃ (n : ι), s t n) (hb : (uniformity β).HasAntitoneBasis V) :
                                      (uniformity (UniformOnFun α β 𝔖)).HasAntitoneBasis fun (n : ι) => UniformOnFun.gen 𝔖 (t n) (V n)

                                      If t n is a monotone sequence of sets in 𝔖 such that each s ∈ 𝔖 is included in some t n and V n is an antitone basis of entourages of β, then UniformOnFun.gen 𝔖 (t n) (V n) is an antitone basis of entourages of α →ᵤ[𝔖] β.

                                      theorem UniformOnFun.isCountablyGenerated_uniformity {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) [(uniformity β).IsCountablyGenerated] {t : Set α} (ht : ∀ (n : ), t n 𝔖) (hmono : Monotone t) (hex : s𝔖, ∃ (n : ), s t n) :
                                      (uniformity (UniformOnFun α β 𝔖)).IsCountablyGenerated
                                      theorem UniformOnFun.hasBasis_nhds_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) {p : ιProp} {s : ιSet (β × β)} (hb : (uniformity β).HasBasis p s) :
                                      (nhds f).HasBasis (fun (Si : Set α × ι) => Si.1 𝔖 p Si.2) fun (Si : Set α × ι) => {g : UniformOnFun α β 𝔖 | (g, f) UniformOnFun.gen 𝔖 Si.1 (s Si.2)}

                                      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 : 𝔖.Nonempty) (h' : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) :
                                      (nhds f).HasBasis (fun (SV : Set α × Set (β × β)) => SV.1 𝔖 SV.2 uniformity β) fun (SV : Set α × Set (β × β)) => {g : UniformOnFun α β 𝔖 | (g, f) UniformOnFun.gen 𝔖 SV.1 SV.2}

                                      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 s.restrict (UniformOnFun.toFun 𝔖))

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

                                      theorem UniformOnFun.uniformity_eq_of_basis {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ιProp} {V : ιSet (β × β)} (h : (uniformity β).HasBasis p V) :
                                      uniformity (UniformOnFun α β 𝔖) = s𝔖, ⨅ (i : ι), ⨅ (_ : p i), Filter.principal (UniformOnFun.gen 𝔖 s (V i))

                                      A version of UniformOnFun.hasBasis_uniformity_of_basis with weaker conclusion and weaker assumptions.

                                      We make no assumptions about the set 𝔖 but conclude only that the uniformity is equal to some indexed infimum.

                                      theorem UniformOnFun.uniformity_eq {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
                                      uniformity (UniformOnFun α β 𝔖) = s𝔖, Vuniformity β, Filter.principal (UniformOnFun.gen 𝔖 s V)
                                      theorem UniformOnFun.gen_mem_uniformity {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (hs : s 𝔖) {V : Set (β × β)} (hV : V uniformity β) :
                                      theorem UniformOnFun.nhds_eq_of_basis {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ιProp} {V : ιSet (β × β)} (h : (uniformity β).HasBasis p V) (f : UniformOnFun α β 𝔖) :
                                      nhds f = s𝔖, ⨅ (i : ι), ⨅ (_ : p i), Filter.principal {g : UniformOnFun α β 𝔖 | xs, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) V i}

                                      A version of UniformOnFun.hasBasis_nhds_of_basis with weaker conclusion and weaker assumptions.

                                      We make no assumptions about the set 𝔖 but conclude only that the neighbourhoods filter is equal to some indexed infimum.

                                      theorem UniformOnFun.nhds_eq {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) :
                                      nhds f = s𝔖, Vuniformity β, Filter.principal {g : UniformOnFun α β 𝔖 | xs, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) V}
                                      theorem UniformOnFun.gen_mem_nhds {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (hs : s 𝔖) {V : Set (β × β)} (hV : V uniformity β) :
                                      {g : UniformOnFun α β 𝔖 | xs, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) V} nhds f
                                      theorem UniformOnFun.uniformContinuous_ofUniformFun {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
                                      UniformContinuous fun (f : UniformFun α β) => (UniformOnFun.ofFun 𝔖) (UniformFun.toFun f)
                                      def UniformOnFun.uniformEquivUniformFun {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (h : Set.univ 𝔖) :
                                      UniformOnFun α β 𝔖 ≃ᵤ UniformFun α β

                                      The uniformity on α →ᵤ[𝔖] β is the same as the uniformity on α →ᵤ β, provided that Set.univ ∈ 𝔖.

                                      Here we formulate it as a UniformEquiv.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        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.uniformContinuous_eval_of_mem_sUnion {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {x : α} (hx : x 𝔖.sUnion) :
                                        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 : αγ) => f x) (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 : αγ) => f x) (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 : αγ) => f x) (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.

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

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

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

                                        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.

                                        Equations
                                        Instances For
                                          theorem UniformOnFun.precomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} {f : γα} (hf : Set.MapsTo (fun (x : Set γ) => f '' x) 𝔗 𝔖) :
                                          UniformContinuous fun (g : UniformOnFun α β 𝔖) => (UniformOnFun.ofFun 𝔗) ((UniformOnFun.toFun 𝔖) 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.

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

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

                                            theorem UniformOnFun.uniformContinuous_restrict_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} :
                                            UniformContinuous (𝔖.sUnion.restrict (UniformOnFun.toFun 𝔖))

                                            The restriction map from α →ᵤ[𝔖] β to ⋃₀ 𝔖 → β is uniformly continuous.

                                            theorem UniformOnFun.uniformContinuous_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} (h : 𝔖.sUnion = 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𝔖, TendstoUniformlyOn ((UniformOnFun.toFun 𝔖) F) ((UniformOnFun.toFun 𝔖) f) p s

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

                                            theorem UniformOnFun.continuous_rng_iff {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} {X : Type u_5} [TopologicalSpace X] {f : XUniformOnFun α β 𝔖} :
                                            Continuous f s𝔖, Continuous (UniformFun.ofFun s.restrict (UniformOnFun.toFun 𝔖) f)
                                            instance UniformOnFun.instCompleteSpace {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [CompleteSpace β] :
                                            Equations
                                            • =
                                            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 (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ).

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            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.

                                              Equations
                                              Instances For
                                                theorem UniformOnFun.isClosed_setOf_continuous_of_le {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) [t : TopologicalSpace α] (h : t s𝔖, TopologicalSpace.coinduced Subtype.val inferInstance) :
                                                IsClosed {f : UniformOnFun α β 𝔖 | Continuous ((UniformOnFun.toFun 𝔖) f)}

                                                Suppose that the topology on α is defined by its restrictions to the sets of 𝔖.

                                                Then the set of continuous functions is closed in the topology of uniform convergence on the sets of 𝔖.

                                                instance UniformFun.instCompleteSpace {α : Type u_1} {β : Type u_2} [UniformSpace β] [CompleteSpace β] :
                                                Equations
                                                • =