Theorems · Definition · Lie groups

IsTopologicalGroup.leftUniformSpace

(G : Type u_1) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → UniformSpace G

The left uniformity on a topological group (as opposed to the right uniformity). Warning: in general the right and left uniformities do not coincide and so one does not obtain a IsUniformGroup structure. Two important special cases where they _do_ coincide are for commutative groups (see isUniformGroup_of_commGroup) and for compact groups (see IsUniformGroup.of_compactSpace).

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

6 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceIsTopologicalGroup