Theorem EMetric.toUniformSpace_ofEDist

Modification history

2026-04-28 22:05
Mathlib/Topology/EMetricSpace/Defs.lean
feat(Topology/EMetricSpace): add ```Weak(Pseudo)EMetricSpace``` (#38105) …
Added EMetric.toUniformSpace_ofEDistView on Github →