| ||||
| ||||
![]() Title:Formalizing the Gromov-Hausdorff Space Authors:Sebastien Gouezel Conference:CICM 2021 Tags:formalization, Gromov-Hausdorff space and Lean 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. Formalizing the Gromov-Hausdorff Space ![]() Formalizing the Gromov-Hausdorff Space | ||||
Copyright © 2002 – 2025 EasyChair |