Theorem PseudoMetric.coe_mk

Modification history

2025-05-13 16:33

Mathlib/Topology/MetricSpace/BundledFun.lean

feat(Topology/MetricSpace): pseudometrics as bundled functions (#23111) …

Added PseudoMetric.coe_mk View on Github →