Equivalence relation identifying two nonempty compact sets which are isometric

This is indeed an equivalence relation

setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ)

The Gromov-Hausdorff space

Map any nonempty compact type to GH_space

A metric space representative of any abstract point in GH_space

Two nonempty compact spaces have the same image in GH_space if and only if they are isometric

Distance on GH_space : the distance between two nonempty compact spaces is the infimum Hausdorff distance between isometric copies of the two spaces in a metric space. For the definition, we only consider embeddings in ℓ^∞(ℝ), but we will prove below that it works for all spaces.

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

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

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

The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space.

In particular, nonempty compacts of a metric space map to GH_space. We register this in the topological_space namespace to take advantage of the notation p.to_GH_space

If there are subsets which are ε1-dense and ε3-dense in two spaces, and isometric up to ε2, then the Gromov-Hausdorff distance between the spaces is bounded by ε1 + ε2/2 + ε3.

The Gromov-Hausdorff space is second countable.

Compactness criterion : a closed set of compact metric spaces is compact if the spaces have a uniformly bounded diameter, and for all ε the number of balls of radius ε required to cover the space is uniformly bounded. This is an equivalence, but we only prove the interesting direction that these conditions imply compactness.

The Gromov-Hausdorff space is complete.