Structures · Topology
IsRightUniformGroup
A right-uniform group is a topological group endowed with the associated
right uniform structure: the uniformity filter 𝓤 G is the inverse image of 𝓝 1 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 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…
Assumed by12
- uniformity_eq_comap_nhds_one
- uniformity_eq_comap_mul_inv_nhds_one
- uniformity_eq_comap_nhds_one_swapped
- tendsto_conj_nhds_one
- Filter.Tendsto.conj_nhds_one
- IsUniformGroup.of_left_right
- comap_conj_nhds_one
- IsRightUniformGroup.uniformity_eq
- IsRightUniformGroup.completeSpace_of_weaklyLocallyCompactSpace
- uniformity_eq_comap_mul_inv_nhds_one_swapped
- QuotientGroup.completeSpace_right
- IsRightUniformGroup.toIsTopologicalGroup