Commit 2024-02-06 13:53 cea4cc6e
View on Github →chore(MetricSpace/HausdorffDistance): split in two (#9809) The file was becoming a bit large (1550 lines). Split in two files of about 900 and 700 lines: the first file contains more basic material, the second file contains all material related to thickenings. Extend the module docstrings by mentioning the main results in this file.