Theorem SeparationQuotient.dist_mk

Modification history

2026-08-25 01:15
Mathlib/Topology/MetricSpace/Basic.lean
feat(Topology/MetricSpace): add distance congruence lemmas (#42893)
Modified SeparationQuotient.dist_mkView on Github →
2024-03-10 19:38
Mathlib/Topology/MetricSpace/Basic.lean
refactor(UniformSpace): drop `separationRel` (#10644) …
Added SeparationQuotient.dist_mkView on Github →