Theorems · Theorem · general topology

GromovHausdorff.hausdorffDist_optimal_le_HD

∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y] {f : GromovHausdorff.Cb✝ X Y},
  f ∈ GromovHausdorff.candidatesB✝ X Y →
    Metric.hausdorffDist (Set.range (GromovHausdorff.optimalGHInjl X Y))
        (Set.range (GromovHausdorff.optimalGHInjr X Y)) ≤
      GromovHausdorff.HD f

For any candidate f, HD(f) is larger than or equal to the Hausdorff distance in the optimal coupling. This follows from the fact that HD of the optimal candidate is exactly the Hausdorff distance in the optimal coupling, although we only prove here the inequality we need.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Cited by

1 results in Mathlib

Foundations

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

Assumes

MetricSpaceCompactSpaceNonemptyMetricSpaceCompactSpaceNonempty