Theorem DiscreteUniformity.eq_principal_idRel

Modification history

2025-03-24 18:39

Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

feat(Topology/UniformSpace/DiscreteUniformity): discrete uniformity (#23067)

Added DiscreteUniformity.eq_principal_idRel View on Github →