mathlib

81f29f90 - chore(topology/metric_space): cleanup Gromov-Hausdorff files (#7936)

chore(topology/metric_space): cleanup Gromov-Hausdorff files (#7936) Rename greek type variables to meaningful uppercase letters. Lint the files. Add a header where needed. Add spaces after forall or exist to conform to current style guide. Absolutely no new mathematical content.