# mathlib3documentation

topology.algebra.uniform_convergence

# Algebraic facts about the topology of uniform convergence #

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

This file contains algebraic compatibility results about the uniform structure of uniform convergence / 𝔖-convergence. They will mostly be useful for defining strong topologies on the space of continuous linear maps between two topological vector spaces.

## Main statements #

• uniform_fun.uniform_group : if G is a uniform group, then α →ᵤ G a uniform group
• uniform_on_fun.uniform_group : if G is a uniform group, then for any 𝔖 : set (set α), α →ᵤ[𝔖] G a uniform group.
• uniform_on_fun.has_continuous_smul_of_image_bounded : let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology induced from α →ᵤ[𝔖] E, is a TVS.

## Implementation notes #

Like in topology/uniform_space/uniform_convergence_topology, we use the type aliases uniform_fun (denoted α →ᵤ β) and uniform_on_fun (denoted α →ᵤ[𝔖] β) for functions from α to β endowed with the structures of uniform convergence and 𝔖-convergence.

## TODO #

• uniform_on_fun.has_continuous_smul_of_image_bounded unnecessarily asks for 𝔖 to be nonempty and directed. This will be easy to solve once we know that replacing 𝔖 by its noncovering bornology (i.e not what bornology currently refers to in mathlib) doesn't change the topology.

## Tags #

uniform convergence, strong dual

@[protected, instance]
def uniform_fun.add_monoid {α : Type u_1} {β : Type u_2} [add_monoid β] :
Equations
@[protected, instance]
def uniform_fun.monoid {α : Type u_1} {β : Type u_2} [monoid β] :
monoid β)
Equations
@[protected, instance]
def uniform_on_fun.monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [monoid β] :
monoid β 𝔖)
Equations
@[protected, instance]
def uniform_on_fun.add_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_monoid β] :
Equations
@[protected, instance]
def uniform_fun.add_comm_monoid {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def uniform_fun.comm_monoid {α : Type u_1} {β : Type u_2} [comm_monoid β] :
Equations
@[protected, instance]
def uniform_on_fun.add_comm_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)}  :
Equations
@[protected, instance]
def uniform_on_fun.comm_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [comm_monoid β] :
comm_monoid β 𝔖)
Equations
@[protected, instance]
def uniform_fun.group {α : Type u_1} {β : Type u_2} [group β] :
group β)
Equations
@[protected, instance]
def uniform_fun.add_group {α : Type u_1} {β : Type u_2} [add_group β] :
Equations
@[protected, instance]
def uniform_on_fun.add_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_group β] :
Equations
@[protected, instance]
def uniform_on_fun.group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [group β] :
group β 𝔖)
Equations
@[protected, instance]
def uniform_fun.comm_group {α : Type u_1} {β : Type u_2} [comm_group β] :
Equations
@[protected, instance]
def uniform_fun.add_comm_group {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def uniform_on_fun.add_comm_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)}  :
Equations
@[protected, instance]
def uniform_on_fun.comm_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [comm_group β] :
comm_group β 𝔖)
Equations
@[protected, instance]
def uniform_fun.module {α : Type u_1} {β : Type u_2} {R : Type u_4} [semiring R] [ β] :
β)
Equations
@[protected, instance]
def uniform_on_fun.module {α : Type u_1} {β : Type u_2} {R : Type u_4} {𝔖 : set (set α)} [semiring R] [ β] :
β 𝔖)
Equations
@[protected, instance]
def uniform_fun.uniform_group {α : Type u_1} {G : Type u_2} [group G]  :

If G is a uniform group, then α →ᵤ G is a uniform group as well.

@[protected, instance]
def uniform_fun.uniform_add_group {α : Type u_1} {G : Type u_2} [add_group G]  :

If G is a uniform additive group, then α →ᵤ G is a uniform additive group as well.

@[protected]
theorem uniform_fun.has_basis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [group G] {p : ι Prop} {b : ι set G} (h : (nhds 1).has_basis p b) :
(nhds 1).has_basis p (λ (i : ι), {f : G | (x : α), f x b i})
@[protected]
theorem uniform_fun.has_basis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [add_group G] {p : ι Prop} {b : ι set G} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis p (λ (i : ι), {f : G | (x : α), f x b i})
@[protected]
theorem uniform_fun.has_basis_nhds_zero {α : Type u_1} {G : Type u_2} [add_group G]  :
(nhds 0).has_basis (λ (V : set G), V nhds 0) (λ (V : set G), {f : α G | (x : α), f x V})
@[protected]
theorem uniform_fun.has_basis_nhds_one {α : Type u_1} {G : Type u_2} [group G]  :
(nhds 1).has_basis (λ (V : set G), V nhds 1) (λ (V : set G), {f : α G | (x : α), f x V})
@[protected, instance]
def uniform_on_fun.uniform_add_group {α : Type u_1} {G : Type u_2} [add_group G] {𝔖 : set (set α)}  :

Let 𝔖 : set (set α). If G is a uniform additive group, then α →ᵤ[𝔖] G is a uniform additive group as well.

@[protected, instance]
def uniform_on_fun.uniform_group {α : Type u_1} {G : Type u_2} [group G] {𝔖 : set (set α)}  :

Let 𝔖 : set (set α). If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group as well.

@[protected]
theorem uniform_on_fun.has_basis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) {p : ι Prop} {b : ι set G} (h : (nhds 1).has_basis p b) :
(nhds 1).has_basis (λ (Si : set α × ι), Si.fst 𝔖 p Si.snd) (λ (Si : set α × ι), {f : 𝔖 | (x : α), x Si.fst f x b Si.snd})
@[protected]
theorem uniform_on_fun.has_basis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [add_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) {p : ι Prop} {b : ι set G} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis (λ (Si : set α × ι), Si.fst 𝔖 p Si.snd) (λ (Si : set α × ι), {f : 𝔖 | (x : α), x Si.fst f x b Si.snd})
@[protected]
theorem uniform_on_fun.has_basis_nhds_one {α : Type u_1} {G : Type u_2} [group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) :
(nhds 1).has_basis (λ (SV : set α × set G), SV.fst 𝔖 SV.snd nhds 1) (λ (SV : set α × set G), {f : 𝔖 | (x : α), x SV.fst f x SV.snd})
@[protected]
theorem uniform_on_fun.has_basis_nhds_zero {α : Type u_1} {G : Type u_2} [add_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) :
(nhds 0).has_basis (λ (SV : set α × set G), SV.fst 𝔖 SV.snd nhds 0) (λ (SV : set α × set G), {f : 𝔖 | (x : α), x SV.fst f x SV.snd})
theorem uniform_on_fun.has_continuous_smul_induced_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [normed_field 𝕜] [ H] [ E] [ E] {𝔖 : set (set α)} [ 𝕜 H E 𝔖)] (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) (φ : hom) (hφ : inducing φ) (h : (u : H) (s : set α), s 𝔖 (φ u '' s)) :

Let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

For convenience, we don't literally ask for H : submodule (α →ᵤ[𝔖] E). Instead, we prove the result for any vector space H equipped with a linear inducing to α →ᵤ[𝔖] E, which is often easier to use. We also state the submodule version as uniform_on_fun.has_continuous_smul_submodule_of_image_bounded.

theorem uniform_on_fun.has_continuous_smul_submodule_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [normed_field 𝕜] [ E] [ E] {𝔖 : set (set α)} (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) (H : E 𝔖)) (h : (u : α E), u H (s : set α), s 𝔖 (u '' s)) :

Let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

If you have a hard time using this lemma, try the one above instead.