Formalizing the Gromov-Hausdorff space
Logic in Computer Science
2021-09-01 v1 Metric Geometry
Abstract
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.
Cite
@article{arxiv.2108.13660,
title = {Formalizing the Gromov-Hausdorff space},
author = {Sébastien Gouëzel},
journal= {arXiv preprint arXiv:2108.13660},
year = {2021}
}