Theorem discreteUniformity_iff_eq_principal_idRel

Modification history

2025-03-24 18:39

Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

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

Added discreteUniformity_iff_eq_principal_idRel View on Github →