Theorems · Definition · general topology

GromovHausdorff.ghDist

(X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [Nonempty X] → [CompactSpace X] → [inst : MetricSpace Y] → [Nonempty Y] → [CompactSpace Y] → ℝ

The Gromov-Hausdorff distance between two nonempty compact metric spaces, equal by definition to the distance of the equivalence classes of these spaces in the Gromov-Hausdorff space.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorff

Cited by

7 results in Mathlib

Foundations

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

Assumes

MetricSpaceNonemptyCompactSpaceMetricSpaceNonemptyCompactSpace