Theorem discreteUniformity_iff_idRel_mem_uniformity

Modification history

2025-03-24 18:39

Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

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

Added discreteUniformity_iff_idRel_mem_uniformity View on Github →