Theorems · Inductive type · Lie groups

IsUniformGroup

(α : Type u_3) → [UniformSpace α] → [Group α] → Prop

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

Cited by

145 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

UniformSpaceGroup