Def GromovHausdorff.premetricOptimalGHDist

Modification history

2023-05-24 09:57

Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

feat: port Topology.MetricSpace.GromovHausdorffRealized (#4206) …

Added GromovHausdorff.premetricOptimalGHDist View on Github →