Theorems · Theorem · general topology

GromovHausdorff.hausdorffDist_optimal

∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y)) (Set.range (GromovHausdorff.optimalGHInjr X Y)) =
    GromovHausdorff.ghDist X Y

The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance, essentially by design.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorff

Cited by

1 results in Mathlib

Foundations

Depth 241 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpaceCompactSpaceNonemptyMetricSpaceCompactSpaceNonempty