Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-15 03:22 81f29f90

View on Github →

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.

Estimated changes