Theorems · Definition · Lie groups

IsTopologicalAddGroup.rightUniformSpace

(G : Type u_1) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [IsTopologicalAddGroup G] → UniformSpace G

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

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

33 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroup