Theorems · Inductive type · Lie groups

IsLeftUniformGroup

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

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

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

8 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

UniformSpaceGroup