Theorems · Inductive type · Lie groups

IsLeftUniformAddGroup

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

A left-uniform additive group is a topological additive group endowed with the associated left uniform structure: the uniformity filter 𝓤 G is the inverse image of 𝓝 0 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 0.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

6 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

UniformSpaceAddGroup