Structures · Topology
IsLeftUniformGroup
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.
- 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…