# 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