# Documentation

Mathlib.Topology.Algebra.UniformConvergence

# Algebraic facts about the topology of uniform convergence #

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 #

• UniformFun.uniform_group : if G is a uniform group, then α →ᵤ G a uniform group
• UniformOnFun.uniform_group : if G is a uniform group, then for any 𝔖 : Set (Set α), α →ᵤ[𝔖] G a uniform group.
• UniformOnFun.continuousSMul_induced_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.IsVonNBounded), then H, equipped with the topology induced from α →ᵤ[𝔖] E, is a TVS.

## Implementation notes #

Like in Topology/UniformSpace/UniformConvergenceTopology, we use the type aliases UniformFun (denoted α →ᵤ β) and UniformOnFun (denoted α →ᵤ[𝔖] β) for functions from α to β endowed with the structures of uniform convergence and 𝔖-convergence.

## TODO #

• UniformOnFun.continuousSMul_induced_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.
• [N. Bourbaki, General Topology, Chapter X][bourbaki1966]
• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

## Tags #

uniform convergence, strong dual