Topology and uniform structure of uniform convergence

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

• uniform convergence on α
• uniform convergence on a specified family 𝔖 of sets of α, also called 𝔖-convergence

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 :

• the topology of compact convergence, when 𝔖 is the set of compacts of α
• the strong topology on the dual of a topological vector space (TVS) E, when 𝔖 is the set of Von Neumann bounded subsets of E
• the weak-* topology on the dual of a TVS E, when 𝔖 is the set of singletons of E.

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

Main definitions

• UniformFun.gen: basis sets for the uniformity of uniform convergence. These are sets of the form S(V) := {(f, g) | ∀ x : α, (f x, g x) ∈ V} for some V : Set (β × β)
• UniformFun.uniformSpace: uniform structure of uniform convergence. This is the UniformSpace on α →ᵤ β whose uniformity is generated by the sets S(V) for V ∈ 𝓤 β. We will denote this uniform space as 𝒰(α, β, uβ), both in the comments and as a local notation in the Lean code, where uβ is the uniform space structure on β. This is declared as an instance on α →ᵤ β.
• UniformOnFun.uniformSpace: uniform structure of 𝔖-convergence, where 𝔖 : Set (Set α). This is the infimum, for S ∈ 𝔖, of the pullback of 𝒰 S β by the map of restriction to S. We will denote it 𝒱(α, β, 𝔖, uβ), where uβ is the uniform space structure on β. This is declared as an instance on α →ᵤ[𝔖] β.

Main statements

Basic properties

• UniformFun.uniformContinuous_eval: evaluation is uniformly continuous on α →ᵤ β.
• UniformFun.t2Space: the topology of uniform convergence on α →ᵤ β is T₂ if β is T₂.
• UniformFun.tendsto_iff_tendstoUniformly: 𝒰(α, β, uβ) is indeed the uniform structure of uniform convergence
• UniformOnFun.uniformContinuous_eval_of_mem: evaluation at a point contained in a set of 𝔖 is uniformly continuous on α →ᵤ[𝔖] β
• UniformOnFun.t2Space_of_covering: the topology of 𝔖-convergence on α →ᵤ[𝔖] β is T₂ if β is T₂ and 𝔖 covers α
• UniformOnFun.tendsto_iff_tendstoUniformlyOn: 𝒱(α, β, 𝔖 uβ) is indeed the uniform structure of 𝔖-convergence

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

• UniformOnFun.mono: let u₁, u₂ be two uniform structures on γ and 𝔖₁ 𝔖₂ : Set (Set α). If u₁ ≤ u₂ and 𝔖₂ ⊆ 𝔖₁ then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).
• UniformOnFun.iInf_eq: if u is a family of uniform structures on γ, then 𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).
• UniformOnFun.comap_eq: if u is a uniform structures on β and f : γ → β, then 𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁).

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)

• UniformOnFun.postcomp_uniformContinuous: if f : γ → β is uniformly continuous, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is uniformly continuous.
• UniformOnFun.postcomp_isUniformInducing: if f : γ → β is a uniform inducing, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is a uniform inducing.
• UniformOnFun.precomp_uniformContinuous: let f : γ → α, 𝔖 : Set (Set α), 𝔗 : Set (Set γ), and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖. Then, the function (fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β) is uniformly continuous.

Isomorphism statements (bundled)

• UniformOnFun.congrRight: turn a uniform isomorphism γ ≃ᵤ β into a uniform isomorphism (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β) by post-composing.
• UniformOnFun.congrLeft: turn a bijection e : γ ≃ α such that we have both ∀ T ∈ 𝔗, e '' T ∈ 𝔖 and ∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗 into a uniform isomorphism (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β) by pre-composing.
• UniformOnFun.uniformEquivPiComm: the natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform isomorphism between α →ᵤ[𝔖] (Π i, δ i) and Π i, α →ᵤ[𝔖] δ i.

Important use cases

• If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group: since (/) : G × G → G is uniformly continuous, UniformOnFun.postcomp_uniformContinuous tells us that ((/) ∘ —) : (α →ᵤ[𝔖] G × G) → (α →ᵤ[𝔖] G) is uniformly continuous. By precomposing with UniformOnFun.uniformEquivProdArrow, this gives that (/) : (α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G) → (α →ᵤ[𝔖] G) is also uniformly continuous
• The transpose of a continuous linear map is continuous for the strong topologies: since continuous linear maps are uniformly continuous and map bounded sets to bounded sets, this is just a special case of UniformOnFun.precomp_uniformContinuous.

TODO

• Show that the uniform structure of 𝔖-convergence is exactly the structure of 𝔖'-convergence, where 𝔖' is the noncovering bornology (i.e not what Bornology currently refers to in mathlib) generated by 𝔖.

References

• N. Bourbaki, General Topology, Chapter X

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

• UniformFun α β = (α → β)

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

• UniformOnFun α β x✝ = (α → β)

def UniformConvergence.«term_→ᵤ_» : Lean.TrailingParserDescr

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.

def UniformConvergence.«term_→ᵤ[_]_» : Lean.TrailingParserDescr

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.

instance instNonemptyUniformFun {α : Type u_1} {β : Type u_2} [Nonempty β] : Nonempty (UniformFun α β)

instance instNonemptyUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Nonempty β] : Nonempty (UniformOnFun α β 𝔖)

instance instSubsingletonUniformFun {α : Type u_1} {β : Type u_2} [Subsingleton β] : Subsingleton (UniformFun α β)

instance instSubsingletonUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Subsingleton β] : Subsingleton (UniformOnFun α β 𝔖)

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 := ⋯ }

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

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

Equations

• UniformOnFun.ofFun 𝔖 = { toFun := fun (x : α → β) => x, invFun := fun (x : UniformOnFun α β 𝔖) => x, left_inv := ⋯, right_inv := ⋯ }

def UniformFun.toFun {α : Type u_1} {β : Type u_2} : UniformFun α β ≃ (α → β)

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

Equations

• UniformFun.toFun = UniformFun.ofFun.symm

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

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

Equations

• UniformOnFun.toFun 𝔖 = (UniformOnFun.ofFun 𝔖).symm

@[simp]

theorem UniformFun.toFun_ofFun {α : Type u_1} {β : Type u_2} (f : α → β) : toFun (ofFun f) = f

@[simp]

theorem UniformFun.ofFun_toFun {α : Type u_1} {β : Type u_2} (f : UniformFun α β) : ofFun (toFun f) = f

@[simp]

theorem UniformOnFun.toFun_ofFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : α → β) : (toFun 𝔖) ((ofFun 𝔖) f) = f

@[simp]

theorem UniformOnFun.ofFun_toFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : UniformOnFun α β 𝔖) : (ofFun 𝔖) ((toFun 𝔖) f) = f

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

• UniformFun.gen α β V = {uv : UniformFun α β × UniformFun α β | ∀ (x : α), (UniformFun.toFun uv.1 x, UniformFun.toFun uv.2 x) ∈ V}

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 (β × β)) : FilterBasis (UniformFun α β × UniformFun α β)

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

• UniformFun.basis α β 𝓕 = ⋯.filterBasis

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

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

Equations

• UniformFun.filter α β 𝓕 = (UniformFun.basis α β 𝓕).filter

def UniformFun.phi (α : Type u_5) (β : Type u_6) (uvx : (UniformFun α β × UniformFun α β) × α) : β × β

Equations

• UniformFun.phi α β uvx = (uvx.1.1 uvx.2, uvx.1.2 uvx.2)

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

def UniformFun.uniformCore (α : Type u_1) (β : Type u_2) [UniformSpace β] : UniformSpace.Core (UniformFun α β)

Core of the uniform structure of uniform convergence.

Equations

• UniformFun.uniformCore α β = UniformSpace.Core.mkOfBasis (UniformFun.basis α β (uniformity β)) ⋯ ⋯ ⋯

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

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

Equations

• UniformFun.uniformSpace α β = UniformSpace.ofCore (UniformFun.uniformCore α β)

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

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

Equations

• UniformFun.topologicalSpace α β = inferInstance

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 ∘ ⇑toFun)

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

@[simp]

theorem UniformFun.mem_gen {α : Type u_1} {β : Type u_5} {f g : UniformFun α β} {V : Set (β × β)} : (f, g) ∈ UniformFun.gen α β V ↔ ∀ (x : α), (toFun f x, toFun g x) ∈ V

theorem UniformFun.mono {α : Type u_1} {γ : Type u_3} : Monotone (@uniformSpace α γ)

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 γ} : uniformSpace α γ = ⨅ (i : ι), 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₁ u₂ : UniformSpace γ} : uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ

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

theorem UniformFun.postcomp_isUniformInducing {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) : IsUniformInducing (⇑ofFun ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑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_isUniformEmbedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) : IsUniformEmbedding (⇑ofFun ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑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 : γ → β} : uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) => f ∘ x) (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 (⇑ofFun ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑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 : γ ≃ᵤ β) : UniformFun α γ ≃ᵤ UniformFun α β

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

Equations

• UniformFun.congrRight e = { toEquiv := Equiv.piCongrRight fun (x : α) => e.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

theorem UniformFun.precomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {f : γ → α} : UniformContinuous fun (g : UniformFun α β) => ofFun (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 : γ ≃ α) : UniformFun γ β ≃ᵤ UniformFun α β

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

Equations

• UniformFun.congrLeft e = { toEquiv := e.arrowCongr (Equiv.refl β), uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

theorem UniformFun.uniformContinuous_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] : UniformContinuous ⇑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 β] : T2Space (UniformFun α β)

The topology of uniform convergence is T₂.

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 (⇑toFun ∘ F) (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

• UniformFun.uniformEquivProdArrow = (Equiv.arrowProdEquivProdArrow α (fun (a : α) => β) fun (a : α) => γ).toUniformEquivOfIsUniformInducing ⋯

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

• UniformFun.uniformEquivPiComm α δ = (Equiv.piComm fun (a : α) => δ).toUniformEquivOfIsUniformInducing ⋯

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

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

theorem UniformFun.uniformSpace_eq_inf_precomp_of_cover {α : Type u_1} (β : Type u_2) [UniformSpace β] {δ₁ : Type u_6} {δ₂ : Type u_7} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (h_cover : Set.range φ₁ ∪ Set.range φ₂ = Set.univ) : uniformSpace α β = UniformSpace.comap (⇑ofFun ∘ (fun (x : α → β) => x ∘ φ₁) ∘ ⇑toFun) (uniformSpace δ₁ β) ⊓ UniformSpace.comap (⇑ofFun ∘ (fun (x : α → β) => x ∘ φ₂) ∘ ⇑toFun) (uniformSpace δ₂ β)

theorem UniformFun.uniformSpace_eq_iInf_precomp_of_cover {α : Type u_1} (β : Type u_2) {ι : Type u_4} [UniformSpace β] {δ : ι → Type u_6} (φ : (i : ι) → δ i → α) (h_cover : ∃ (I : Set ι), I.Finite ∧ ⋃ i ∈ I, Set.range (φ i) = Set.univ) : uniformSpace α β = ⨅ (i : ι), UniformSpace.comap (⇑ofFun ∘ (fun (x : α → β) => x ∘ φ i) ∘ ⇑toFun) (uniformSpace (δ i) β)

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

• UniformOnFun.gen 𝔖 S V = {uv : UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖 | ∀ x ∈ S, ((UniformOnFun.toFun 𝔖) uv.1 x, (UniformOnFun.toFun 𝔖) uv.2 x) ∈ V}

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 S' : Set α} {V V' : Set (β × β)} (hS : S' ⊆ S) (hV : V ⊆ V') : UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' 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 (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) (𝓑 : 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 α)) : UniformSpace (UniformOnFun α β 𝔖)

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 uβ is the uniform structure on β.

Equations

• UniformOnFun.uniformSpace α β 𝔖 = ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformFun.uniformSpace (↑s) β)

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

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

Equations

• UniformOnFun.topologicalSpace α β 𝔖 = UniformSpace.toTopologicalSpace

theorem UniformOnFun.topologicalSpace_eq (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : topologicalSpace α β 𝔖 = ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(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 (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {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 (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {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 (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) : (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 (x1 x2 : Set α) => x1 ⊆ x2) 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 (x1 x2 : ι) => x1 ≤ x2] {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 (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {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 (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) : (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 ∘ ⇑(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 ∈ 𝔖, ⨅ V ∈ uniformity β, 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 β) : UniformOnFun.gen 𝔖 s V ∈ uniformity (UniformOnFun α β 𝔖)

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 α β 𝔖 | ∀ x ∈ s, ((toFun 𝔖) f x, (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 ∈ 𝔖, ⨅ V ∈ uniformity β, Filter.principal {g : UniformOnFun α β 𝔖 | ∀ x ∈ s, ((toFun 𝔖) f x, (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 α β 𝔖 | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈ nhds f

theorem UniformOnFun.uniformContinuous_ofUniformFun {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : UniformContinuous fun (f : UniformFun α β) => (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.

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

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 ∈ 𝔖) : UniformContinuous (Function.eval x ∘ ⇑(toFun 𝔖))

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 ∈ ⋃₀ 𝔖) : UniformContinuous (Function.eval x ∘ ⇑(toFun 𝔖))

theorem UniformOnFun.uniformContinuous_eval {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} (h : ⋃₀ 𝔖 = Set.univ) (x : α) : UniformContinuous (Function.eval x ∘ ⇑(toFun 𝔖))

theorem UniformOnFun.iInf_eq {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : Set (Set α)} {u : ι → UniformSpace γ} : uniformSpace α γ 𝔖 = ⨅ (i : ι), 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₁ u₂ : UniformSpace γ} : uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ 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 : γ → β} : uniformSpace α γ 𝔖 = UniformSpace.comap (fun (x : α → γ) => f ∘ x) (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 (⇑(ofFun 𝔖) ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑(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_isUniformInducing {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) : IsUniformInducing (⇑(ofFun 𝔖) ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑(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_isUniformEmbedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) : IsUniformEmbedding (⇑(ofFun 𝔖) ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑(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

• UniformOnFun.congrRight e = { toEquiv := Equiv.piCongrRight fun (_a : α) => e.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

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 α β 𝔖) => (ofFun 𝔗) ((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

• UniformOnFun.congrLeft e he he' = { toEquiv := e.arrowCongr (Equiv.refl β), uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

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_restrict_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} : UniformContinuous ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖))

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

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

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.continuousAt_eval₂ {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] {f : UniformOnFun α β 𝔖} {x : α} (h𝔖 : ∃ V ∈ 𝔖, V ∈ nhds x) (hc : ContinuousAt ((toFun 𝔖) f) x) : ContinuousAt (fun (fx : UniformOnFun α β 𝔖 × α) => (toFun 𝔖) fx.1 fx.2) (f, x)

If f : α →ᵤ[𝔖] β is continuous at x and x admits a neighbourhood V ∈ 𝔖, then evaluation of g : α →ᵤ[𝔖] β at y : α is continuous in (g, y) at (f, x).

theorem UniformOnFun.continuousOn_eval₂ {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] (h𝔖 : ∀ (x : α), ∃ V ∈ 𝔖, V ∈ nhds x) : ContinuousOn (fun (fx : UniformOnFun α β 𝔖 × α) => (toFun 𝔖) fx.1 fx.2) {fx : UniformOnFun α β 𝔖 × α | ContinuousAt ((toFun 𝔖) fx.1) fx.2}

If each point of α admits a neighbourhood V ∈ 𝔖, then the evaluation of f : α →ᵤ[𝔖] β at x : α is continuous in (f, x) on the set of (f, x) such that f is continuous at x.

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 (⇑(toFun 𝔖) ∘ F) ((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 : X → UniformOnFun α β 𝔖} : Continuous f ↔ ∀ s ∈ 𝔖, Continuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖) ∘ f)

instance UniformOnFun.instCompleteSpace {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [CompleteSpace β] : CompleteSpace (UniformOnFun α β 𝔖)

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.

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

• UniformOnFun.uniformEquivPiComm 𝔖 δ = (Equiv.piComm fun (a : α) => δ).toUniformEquivOfIsUniformInducing ⋯

theorem UniformOnFun.isClosed_setOf_continuous {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] (h : Topology.IsCoherentWith 𝔖) : IsClosed {f : UniformOnFun α β 𝔖 | Continuous ((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 𝔖.

theorem UniformOnFun.uniformSpace_eq_inf_precomp_of_cover {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {δ₁ : Type u_5} {δ₂ : Type u_6} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂)) (h_image₁ : Set.MapsTo (fun (x : Set δ₁) => φ₁ '' x) 𝔗₁ 𝔖) (h_image₂ : Set.MapsTo (fun (x : Set δ₂) => φ₂ '' x) 𝔗₂ 𝔖) (h_preimage₁ : Set.MapsTo (fun (x : Set α) => φ₁ ⁻¹' x) 𝔖 𝔗₁) (h_preimage₂ : Set.MapsTo (fun (x : Set α) => φ₂ ⁻¹' x) 𝔖 𝔗₂) (h_cover : ∀ S ∈ 𝔖, S ⊆ Set.range φ₁ ∪ Set.range φ₂) : uniformSpace α β 𝔖 = UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun (x : α → β) => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓ UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun (x : α → β) => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)

theorem UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) {δ : ι → Type u_5} (φ : (i : ι) → δ i → α) (𝔗 : (i : ι) → Set (Set (δ i))) (h_image : ∀ (i : ι), Set.MapsTo (fun (x : Set (δ i)) => φ i '' x) (𝔗 i) 𝔖) (h_preimage : ∀ (i : ι), Set.MapsTo (fun (x : Set α) => φ i ⁻¹' x) 𝔖 (𝔗 i)) (h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, Set.range (φ i)) : uniformSpace α β 𝔖 = ⨅ (i : ι), UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun (x : α → β) => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))

instance UniformFun.instCompleteSpace {α : Type u_1} {β : Type u_2} [UniformSpace β] [CompleteSpace β] : CompleteSpace (UniformFun α β)

theorem UniformContinuousOn.comp_tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {p : Filter ι} (s : Set β) (F : ι → α → β) (f : α → β) (hF : ∀ (i : ι) (x : α), F i x ∈ s) (hf : ∀ (x : α), f x ∈ s) {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) : TendstoUniformly (fun (i : ι) (x : α) => g (F i x)) (fun (x : α) => g (f x)) p

Composing on the left by a uniformly continuous function preserves uniform convergence

theorem UniformContinuousOn.comp_tendstoUniformly_eventually {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {p : Filter ι} (s : Set β) (F : ι → α → β) (f : α → β) (hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s) (hf : ∀ (x : α), f x ∈ s) {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) : TendstoUniformly (fun (i : ι) (x : α) => g (F i x)) (fun (x : α) => g (f x)) p