Structures · Topology
IsRightUniformAddGroup
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.
- 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 by11
- uniformity_eq_comap_nhds_zero
- uniformity_eq_comap_nhds_zero_swapped
- uniformity_eq_comap_add_neg_nhds_zero
- tendsto_addConj_nhds_zero
- comap_addConj_nhds_zero
- IsRightUniformAddGroup.uniformity_eq
- IsRightUniformAddGroup.toIsTopologicalAddGroup
- IsRightUniformAddGroup.completeSpace_of_weaklyLocallyCompactSpace
- Filter.Tendsto.addConj_nhds_zero
- uniformity_eq_comap_add_neg_nhds_zero_swapped
- QuotientAddGroup.completeSpace_right