Structures · Topology

IsUniformAddGroup

A uniform additive group is an additive group in which addition and negation are uniformly continuous. IsUniformAddGroup G is equivalent to the fact that G is a topological additive group, and the uniformity coincides with both the associated left and right uniformities (see IsUniformAddGroup.isRightUniformAddGroup, IsUniformAddGroup.isLeftUniformAddGroup and IsUniformAddGroup.of_left_right). Since there are topological groups where these two uniformities do not coincide, not all topological groups admit a uniform group structure in this sense. This is however the case for commutative groups, which are the main motivation for the existence of this typeclass.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Shape

One type argument · adds uniformContinuous_sub