Commit 2023-05-24 09:57 1164db87

View on Github →

feat: port Topology.MetricSpace.GromovHausdorffRealized (#4206) Proof of dist_mem_candidates has been simplified

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

added def GromovHausdorff.HD

added theorem GromovHausdorff.HD_below_aux1

added theorem GromovHausdorff.HD_below_aux2

added theorem GromovHausdorff.HD_candidatesBDist_le

added def GromovHausdorff.OptimalGHCoupling

added def GromovHausdorff.candidates

added def GromovHausdorff.candidatesBDist

added theorem GromovHausdorff.candidatesBDist_mem_candidatesB

added def GromovHausdorff.candidatesBOfCandidates

added theorem GromovHausdorff.candidatesBOfCandidates_mem

added theorem GromovHausdorff.hausdorffDist_optimal_le_HD

added theorem GromovHausdorff.isometry_optimalGHInjl

added theorem GromovHausdorff.isometry_optimalGHInjr

added def GromovHausdorff.optimalGHInjl

added def GromovHausdorff.optimalGHInjr

added def GromovHausdorff.premetricOptimalGHDist