Download PDFOpen PDF in browserFormalizing the Gromov-Hausdorff SpaceEasyChair Preprint no. 61797 pages•Date: July 28, 2021AbstractThe 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
|