Structures · Topology

IsUniformGroup

A uniform group is a group in which multiplication and inversion are uniformly continuous. IsUniformGroup G is equivalent to the fact that G is a topological group, and the uniformity coincides with both the associated left and right uniformities (see IsUniformGroup.isRightUniformGroup, IsUniformGroup.isLeftUniformGroup and IsUniformGroup.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_div