Theorems · Theorem · general topology

GromovHausdorff.ghDist_le_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] {γ : Type w} [inst_6 : MetricSpace γ]
  {Φ : X → γ} {Ψ : Y → γ},
  Isometry Φ → Isometry Ψ → GromovHausdorff.ghDist X Y ≤ Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)

The Gromov-Hausdorff distance between two spaces is bounded by the Hausdorff distance of isometric copies of the spaces, in any metric space.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorff

Cited by

3 results in Mathlib

Foundations

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

Assumes

MetricSpaceCompactSpaceNonemptyMetricSpaceCompactSpaceNonemptyMetricSpace