Def PseudoEMetricSpace.toPseudoMetricSpaceOfDist
Modification history
2024-05-07 01:05
Mathlib/Topology/MetricSpace/PseudoMetric.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted PseudoEMetricSpace.toPseudoMetricSpaceOfDistView on Github →