Def GromovHausdorff.candidatesBDist

Modification history

2024-02-17 16:56

Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

chore(Topology): `Inhabited` -> `Nonempty` (#10647)

Modified GromovHausdorff.candidatesBDist View on Github →

2023-05-24 09:57

Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

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

Added GromovHausdorff.candidatesBDist View on Github →