Theorems · Inductive type · Lie groups

IsRightUniformGroup

(G : Type u_7) → [UniformSpace G] → [Group G] → Prop

A right-uniform group is a topological group endowed with the associated right uniform structure: the uniformity filter 𝓤 G is the inverse image of 𝓝 1 by the map (x, y) ↦ y * x⁻¹. In other words, we declare that two points x and y are infinitely close precisely when y * x⁻¹ is infinitely close to 1.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

11 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

UniformSpaceGroup