Structures · Topology
IsLeftUniformAddGroup
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.
- Shape
- One type argument · adds uniformity_eq
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…