Theorem SeparationQuotient.dist_mk

Modification history

2024-03-10 19:38
Mathlib/Topology/MetricSpace/Basic.lean
refactor(UniformSpace): drop `separationRel` (#10644) …
Added SeparationQuotient.dist_mkView on Github →