Theorems · Theorem · general topology

GromovHausdorff.ghDist_eq_hausdorffDist

∀ (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],
  ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ GromovHausdorff.ghDist X Y = Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)

The Gromov-Hausdorff distance can also be realized by a coupling in ℓ^∞(ℝ), by embedding the optimal coupling through its Kuratowski embedding.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorff

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpaceCompactSpaceNonemptyMetricSpaceCompactSpaceNonempty