# mathlibdocumentation

topology.uniform_space.uniform_convergence_topology

# Topology and uniform structure of uniform convergence #

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

• uniform convergence on α (in the uniform_convergence namespace)
• uniform convergence on a specified family 𝔖 of sets of α (in the uniform_convergence_on namespace), also called 𝔖-convergence

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 TVS E, when 𝔖 is the set of Von Neuman bounded subsets of E
• the weak-* topology on the dual of a TVS E, when 𝔖 is the set of singletons of E.

## Main definitions #

• uniform_convergence.gen : basis sets for the uniformity of uniform convergence
• uniform_convergence.uniform_space : uniform structure of uniform convergence
• uniform_convergence_on.uniform_space : uniform structure of 𝔖-convergence

## Main statements #

• uniform_convergence.uniform_continuous_eval : evaluation is uniformly continuous

• uniform_convergence.t2_space : the topology of uniform convergence on α → β is T2 if β is T2.

• uniform_convergence.tendsto_iff_tendsto_uniformly : uniform_convergence.uniform_space is indeed the uniform structure of uniform convergence

• uniform_convergence_on.uniform_continuous_eval_of_mem : evaluation at a point contained in a set of 𝔖 is uniformly continuous

• uniform_convergence.t2_space : the topology of 𝔖-convergence on α → β is T2 if β is T2 and 𝔖 covers α

• uniform_convergence_on.tendsto_iff_tendsto_uniformly_on : uniform_convergence_on.uniform_space is indeed the uniform structure of 𝔖-convergence

## Implementation details #

We do not declare these structures as instances, since they would conflict with Pi.uniform_space.

## TODO #

• Show that the uniform structure of 𝔖-convergence is exactly the structure of 𝔖'-convergence, where 𝔖' is the bornology generated by 𝔖.
• Add a type synonym for α → β endowed with the structures of uniform convergence

## Tags #

uniform convergence

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

Basis sets for the uniformity of uniform convergence

Equations
• = {uv : (α → β) × (α → β) | ∀ (x : α), (uv.fst x, uv.snd x) V}
@[protected]
theorem uniform_convergence.is_basis_gen (α : Type u_1) (β : Type u_2)  :
filter.is_basis (λ (V : set × β)), V
@[protected]
def uniform_convergence.uniformity_basis (α : Type u_1) (β : Type u_2)  :
filter_basis ((α → β) × (α → β))

Filter basis for the uniformity of uniform convergence

Equations
@[protected]
def uniform_convergence.uniform_core (α : Type u_1) (β : Type u_2)  :
uniform_space.core (α → β)

Core of the uniform structure of uniform convergence

Equations
@[protected]
def uniform_convergence.uniform_space (α : Type u_1) (β : Type u_2)  :
uniform_space (α → β)

Uniform structure of uniform convergence

Equations
@[protected]
theorem uniform_convergence.has_basis_uniformity (α : Type u_1) (β : Type u_2)  :
(uniformity (α → β)).has_basis (λ (V : set × β)), V
@[protected]
def uniform_convergence.topological_space (α : Type u_1) (β : Type u_2)  :
topological_space (α → β)

Topology of uniform convergence

Equations
@[protected]
theorem uniform_convergence.has_basis_nhds (α : Type u_1) (β : Type u_2) {f : α → β}  :
(nhds f).has_basis (λ (V : set × β)), V (λ (V : set × β)), {g : α → β | (g, f) V})
theorem uniform_convergence.uniform_continuous_eval {α : Type u_1} (β : Type u_2) (x : α) :
theorem uniform_convergence.t2_space {α : Type u_1} {β : Type u_2} [t2_space β] :
t2_space (α → β)
@[protected]
theorem uniform_convergence.le_Pi {α : Type u_1} {β : Type u_2}  :
Pi.uniform_space (λ (_x : α), β)
@[protected]
theorem uniform_convergence.tendsto_iff_tendsto_uniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι}  :
(nhds f) p
@[protected]
def uniform_convergence_on.uniform_space (α : Type u_1) (β : Type u_2) (𝔖 : set (set α)) :
uniform_space (α → β)

Uniform structure of uniform convergence on the sets of 𝔖.

Equations
@[protected]
def uniform_convergence_on.topological_space (α : Type u_1) (β : Type u_2) (𝔖 : set (set α)) :
topological_space (α → β)

Topology of uniform convergence on the sets of 𝔖.

Equations
@[protected]
theorem uniform_convergence_on.topological_space_eq (α : Type u_1) (β : Type u_2) (𝔖 : set (set α)) :
= ⨅ (s : set α) (hs : s 𝔖), topological_space.induced (λ (f : α → β), s.restrict f)
@[protected]
theorem uniform_convergence_on.uniform_continuous_restrict (α : Type u_1) (β : Type u_2) (𝔖 : set (set α)) {s : set α} (h : s 𝔖) :
@[protected]
theorem uniform_convergence_on.uniform_space_antitone (α : Type u_1) (β : Type u_2)  :
theorem uniform_convergence_on.uniform_continuous_eval_of_mem {α : Type u_1} (β : Type u_2) (𝔖 : set (set α)) {s : set α} {x : α} (hxs : x s) (hs : s 𝔖) :
theorem uniform_convergence_on.t2_space_of_covering {α : Type u_1} {β : Type u_2} (𝔖 : set (set α)) [t2_space β] (h : ⋃₀ 𝔖 = set.univ) :
t2_space (α → β)
@[protected]
theorem uniform_convergence_on.le_Pi_of_covering {α : Type u_1} {β : Type u_2} (𝔖 : set (set α)) (h : ⋃₀ 𝔖 = set.univ) :
Pi.uniform_space (λ (_x : α), β)
@[protected]
theorem uniform_convergence_on.tendsto_iff_tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} (𝔖 : set (set α)) {F : ι → α → β} {f : α → β} {p : filter ι} :
(nhds f) ∀ (s : set α), s 𝔖 p s