Download PDFOpen PDF in browser

Formalizing the Gromov-Hausdorff Space

EasyChair Preprint no. 6179

7 pagesDate: July 28, 2021


The Gromov-Hausdorff space is usually defined in textbooks as ``the space of all compact metric spaces up to isometry''. We describe a formalization of this notion in the Lean proof assistant, insisting on how we need to depart from the usual informal viewpoint of mathematicians on this object to get a rigorous formalization.

Keyphrases: formalization, Gromov-Hausdorff space, Lean

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Sébastien Gouëzel},
  title = {Formalizing the Gromov-Hausdorff Space},
  howpublished = {EasyChair Preprint no. 6179},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser