Theorems · Inductive type · Lie groups

IsRightUniformAddGroup

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

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

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

9 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

UniformSpaceAddGroup