mathlib3 documentation

topology.uniform_space.uniform_convergence_topology

Topology and uniform structure of uniform convergence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 uniform_fun α β (denoted α →ᵤ β) and uniform_on_fun α β 𝔖 (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 uniform_spaces 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 uniform_convergence.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

@[nolint]
def uniform_on_fun (α : 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 uniform_on_fun
@[protected, instance]
def uniform_fun.nonempty {α : Type u_1} {β : Type u_2} [nonempty β] :
@[protected, instance]
def uniform_on_fun.nonempty {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [nonempty β] :
def uniform_fun.of_fun {α : Type u_1} {β : Type u_2} :
β) uniform_fun α β

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

Equations
def uniform_on_fun.of_fun {α : Type u_1} {β : Type u_2} (𝔖 : set (set α)) :
β) uniform_on_fun α β 𝔖

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

Equations
def uniform_fun.to_fun {α : Type u_1} {β : Type u_2} :
uniform_fun α β β)

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

Equations
def uniform_on_fun.to_fun {α : Type u_1} {β : Type u_2} (𝔖 : set (set α)) :
uniform_on_fun α β 𝔖 β)

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

Equations
@[protected]
def uniform_fun.gen (α : Type u_1) (β : Type u_2) (V : set × β)) :

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
@[protected]
theorem uniform_fun.is_basis_gen (α : Type u_1) (β : Type u_2) (𝓑 : filter × β)) :
filter.is_basis (λ (V : set × β)), V 𝓑) (uniform_fun.gen α β)

If 𝓕 is a filter on β × β, then the set of all uniform_convergence.gen α β V for V ∈ 𝓕 is a filter basis on (α →ᵤ β) × (α →ᵤ β). This will only be applied to 𝓕 = 𝓤 β when β is equipped with a uniform_space 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 uniform_convergence.gc).

@[protected]
def uniform_fun.basis (α : Type u_1) (β : Type u_2) (𝓕 : filter × β)) :

For 𝓕 : filter (β × β), this is the set of all uniform_convergence.gen α β V for V ∈ 𝓕 as a bundled filter_basis over (α →ᵤ β) × (α →ᵤ β). This will only be applied to 𝓕 = 𝓤 β when β is equipped with a uniform_space 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 uniform_convergence.gc).

Equations
@[protected]
def uniform_fun.filter (α : Type u_1) (β : Type u_2) (𝓕 : filter × β)) :

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

Equations
@[protected]
theorem uniform_fun.gc (α : Type u_1) (β : Type u_2) :
galois_connection (λ (𝓐 : filter (uniform_fun α β × uniform_fun α β)), filter.map ((λ (α : Type u_1) (β : Type u_2) (uvx : (uniform_fun α β × uniform_fun α β) × α), (uvx.fst.fst uvx.snd, uvx.fst.snd uvx.snd)) α β) (𝓐.prod )) (λ (𝓕 : filter × β)), uniform_fun.filter α β 𝓕)

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

@[protected]

Core of the uniform structure of uniform convergence.

Equations
@[protected, instance]
def uniform_fun.uniform_space (α : Type u_1) (β : Type u_2) [uniform_space β] :

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

Equations
@[protected, instance]

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

Equations
@[protected]
theorem uniform_fun.has_basis_uniformity (α : Type u_1) (β : Type u_2) [uniform_space β] :
(uniformity (uniform_fun α β)).has_basis (λ (V : set × β)), V uniformity β) (uniform_fun.gen α β)

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

@[protected]
theorem uniform_fun.has_basis_uniformity_of_basis (α : Type u_1) (β : Type u_2) [uniform_space β] {ι : Sort u_3} {p : ι Prop} {s : ι set × β)} (h : (uniformity β).has_basis 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).

@[protected]
theorem uniform_fun.has_basis_nhds_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [uniform_space β] (f : uniform_fun α β) {p : ι Prop} {s : ι set × β)} (h : (uniformity β).has_basis p s) :
(nhds f).has_basis p (λ (i : ι), {g : uniform_fun α β | (f, g) uniform_fun.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 𝓤 β.

@[protected]
theorem uniform_fun.has_basis_nhds (α : Type u_1) (β : Type u_2) [uniform_space β] (f : uniform_fun α β) :
(nhds f).has_basis (λ (V : set × β)), V uniformity β) (λ (V : set × β)), {g : uniform_fun α β | (f, g) uniform_fun.gen α β V})

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

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

@[protected]
theorem uniform_fun.mono {α : Type u_1} {γ : Type u_3} :

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

@[protected]
theorem uniform_fun.infi_eq {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {u : ι uniform_space γ} :

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

@[protected]

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

@[protected]
theorem uniform_fun.comap_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {f : γ β} :

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

@[protected]

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

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

@[protected]

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.

@[protected]
def uniform_fun.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] [uniform_space γ] (e : γ ≃ᵤ β) :

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

Equations
@[protected]
theorem uniform_fun.precomp_uniform_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {f : γ α} :

Pre-composition by a 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.

@[protected]
def uniform_fun.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] (e : γ α) :

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

Equations
@[protected, instance]
def uniform_fun.t2_space {α : Type u_1} {β : Type u_2} [uniform_space β] [t2_space β] :

The topology of uniform convergence is T₂.

@[protected]

The natural map uniform_fun.to_fun 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.

@[protected]
theorem uniform_fun.tendsto_iff_tendsto_uniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : filter ι} [uniform_space β] {F : ι uniform_fun α β} {f : uniform_fun α β} :

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

@[protected]
def uniform_fun.uniform_equiv_prod_arrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] [uniform_space γ] :

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

Equations
@[protected]
def uniform_fun.uniform_equiv_Pi_comm (α : Type u_1) {ι : Type u_4} (δ : ι Type u_5) [Π (i : ι), uniform_space (δ i)] :
uniform_fun α (Π (i : ι), δ i) ≃ᵤ Π (i : ι), uniform_fun α (δ i)

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

Equations
@[protected]
def uniform_on_fun.gen {α : Type u_1} {β : Type u_2} (𝔖 : set (set α)) (S : set α) (V : set × β)) :
set (uniform_on_fun α β 𝔖 × uniform_on_fun α β 𝔖)

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
@[protected]
theorem uniform_on_fun.gen_eq_preimage_restrict {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} (S : set α) (V : set × β)) :

For S : set α and V : set (β × β), we have uniform_on_fun.gen 𝔖 S V = (S.restrict × S.restrict) ⁻¹' (uniform_fun.gen S β V). This is the crucial fact for proving that the family uniform_on_fun.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.

@[protected]
theorem uniform_on_fun.gen_mono {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} {S S' : set α} {V V' : set × β)} (hS : S' S) (hV : V V') :

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

@[protected]
theorem uniform_on_fun.is_basis_gen {α : Type u_1} {β : Type u_2} (𝔖 : set (set α)) (h : 𝔖.nonempty) (h' : directed_on has_subset.subset 𝔖) (𝓑 : filter_basis × β)) :
filter.is_basis (λ (SV : set α × set × β)), SV.fst 𝔖 SV.snd 𝓑) (λ (SV : set α × set × β)), uniform_on_fun.gen 𝔖 SV.fst SV.snd)

If 𝔖 : set (set α) is nonempty and directed and 𝓑 is a filter basis on β × β, then the family uniform_on_fun.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 α →ᵤ[𝔖] β.

@[protected, instance]
def uniform_on_fun.uniform_space (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : 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
@[protected, instance]
def uniform_on_fun.topological_space (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) :

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

Equations
@[protected]

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.

@[protected]
theorem uniform_on_fun.has_basis_uniformity_of_basis_aux₁ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [uniform_space β] (𝔖 : set (set α)) {p : ι Prop} {s : ι set × β)} (hb : (uniformity β).has_basis p s) (S : set α) :
(uniformity (uniform_on_fun α β 𝔖)).has_basis p (λ (i : ι), uniform_on_fun.gen 𝔖 S (s i))
@[protected]
theorem uniform_on_fun.has_basis_uniformity_of_basis_aux₂ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [uniform_space β] (𝔖 : set (set α)) (h : directed_on has_subset.subset 𝔖) {p : ι Prop} {s : ι set × β)} (hb : (uniformity β).has_basis p s) :
@[protected]
theorem uniform_on_fun.has_basis_uniformity_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [uniform_space β] (𝔖 : set (set α)) (h : 𝔖.nonempty) (h' : directed_on has_subset.subset 𝔖) {p : ι Prop} {s : ι set × β)} (hb : (uniformity β).has_basis p s) :
(uniformity (uniform_on_fun α β 𝔖)).has_basis (λ (Si : set α × ι), Si.fst 𝔖 p Si.snd) (λ (Si : set α × ι), uniform_on_fun.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.

@[protected]
theorem uniform_on_fun.has_basis_uniformity (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) (h : 𝔖.nonempty) (h' : directed_on has_subset.subset 𝔖) :
(uniformity (uniform_on_fun α β 𝔖)).has_basis (λ (SV : set α × set × β)), SV.fst 𝔖 SV.snd uniformity β) (λ (SV : set α × set × β)), uniform_on_fun.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.

@[protected]
theorem uniform_on_fun.has_basis_nhds_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [uniform_space β] (𝔖 : set (set α)) (f : uniform_on_fun α β 𝔖) (h : 𝔖.nonempty) (h' : directed_on has_subset.subset 𝔖) {p : ι Prop} {s : ι set × β)} (hb : (uniformity β).has_basis p s) :
(nhds f).has_basis (λ (Si : set α × ι), Si.fst 𝔖 p Si.snd) (λ (Si : set α × ι), {g : uniform_on_fun α β 𝔖 | (g, f) uniform_on_fun.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 𝓤 β.

@[protected]
theorem uniform_on_fun.has_basis_nhds (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) (f : uniform_on_fun α β 𝔖) (h : 𝔖.nonempty) (h' : directed_on has_subset.subset 𝔖) :
(nhds f).has_basis (λ (SV : set α × set × β)), SV.fst 𝔖 SV.snd uniformity β) (λ (SV : set α × set × β)), {g : uniform_on_fun α β 𝔖 | (g, f) uniform_on_fun.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.

@[protected]

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

@[protected]
theorem uniform_on_fun.mono {α : Type u_1} {γ : Type u_3} ⦃u₁ u₂ : uniform_space γ⦄ (hu : u₁ u₂) ⦃𝔖₁ 𝔖₂ : set (set α) (h𝔖 : 𝔖₂ 𝔖₁) :

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

theorem uniform_on_fun.uniform_continuous_eval_of_mem {α : Type u_1} (β : Type u_2) {s : set α} [uniform_space β] (𝔖 : set (set α)) {x : α} (hxs : x s) (hs : s 𝔖) :

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

@[protected]
theorem uniform_on_fun.infi_eq {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : set (set α)} {u : ι uniform_space γ} :

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

@[protected]
theorem uniform_on_fun.inf_eq {α : Type u_1} {γ : Type u_3} {𝔖 : set (set α)} {u₁ u₂ : uniform_space γ} :

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

@[protected]
theorem uniform_on_fun.comap_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {𝔖 : set (set α)} {f : γ β} :

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

@[protected]

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

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

@[protected]
theorem uniform_on_fun.postcomp_uniform_inducing {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {𝔖 : set (set α)} [uniform_space γ] {f : γ β} (hf : uniform_inducing f) :

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 (λ g, f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is a uniform inducing.

@[protected]
def uniform_on_fun.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {𝔖 : set (set α)} [uniform_space γ] (e : γ ≃ᵤ β) :
uniform_on_fun α γ 𝔖 ≃ᵤ uniform_on_fun α β 𝔖

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

Equations
@[protected]
theorem uniform_on_fun.precomp_uniform_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {𝔖 : set (set α)} {𝔗 : set (set γ)} {f : γ α} (hf : 𝔗 set.image f ⁻¹' 𝔖) :

Let f : γ → α, 𝔖 : set (set α), 𝔗 : set (set γ), and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖. Then, the function (λ 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 𝔖.

@[protected]
def uniform_on_fun.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {𝔖 : set (set α)} {𝔗 : set (set γ)} (e : γ α) (he : 𝔗 set.image e ⁻¹' 𝔖) (he' : 𝔖 set.preimage e ⁻¹' 𝔗) :
uniform_on_fun γ β 𝔗 ≃ᵤ uniform_on_fun α β 𝔖

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

Equations
theorem uniform_on_fun.t2_space_of_covering {α : Type u_1} {β : Type u_2} [uniform_space β] {𝔖 : set (set α)} [t2_space β] (h : ⋃₀ 𝔖 = set.univ) :

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

@[protected]

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

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

@[protected]
theorem uniform_on_fun.tendsto_iff_tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : filter ι} [uniform_space β] {𝔖 : set (set α)} {F : ι uniform_on_fun α β 𝔖} {f : uniform_on_fun α β 𝔖} :
filter.tendsto F p (nhds f) (s : set α), s 𝔖 tendsto_uniformly_on F f p s

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

@[protected]
def uniform_on_fun.uniform_equiv_prod_arrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space β] {𝔖 : set (set α)} [uniform_space γ] :
uniform_on_fun α × γ) 𝔖 ≃ᵤ uniform_on_fun α β 𝔖 × uniform_on_fun α γ 𝔖

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

Equations
@[protected]
def uniform_on_fun.uniform_equiv_Pi_comm {α : Type u_1} {ι : Type u_4} (𝔖 : set (set α)) (δ : ι Type u_5) [Π (i : ι), uniform_space (δ i)] :
uniform_on_fun α (Π (i : ι), δ i) 𝔖 ≃ᵤ Π (i : ι), uniform_on_fun α (δ i) 𝔖

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

Equations