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

Modified src/topology/metric_space/gluing.lean

modified def metric.glue_dist

modified theorem metric.glue_dist_glued_points

modified def metric.glue_metric_approx

modified def metric.glue_premetric

modified def metric.inductive_limit

modified def metric.inductive_limit_dist

modified theorem metric.inductive_limit_dist_eq_dist

modified def metric.inductive_premetric

modified theorem metric.isometry_on_inl

modified theorem metric.isometry_on_inr

modified def metric.metric_space_sum

modified def metric.sum.dist

modified theorem metric.sum.dist_eq

modified theorem metric.sum.dist_eq_glue_dist

modified theorem metric.sum.one_dist_le'

modified theorem metric.sum.one_dist_le

modified def metric.to_glue_l

modified def metric.to_glue_r

modified def metric.to_inductive_limit

modified theorem metric.to_inductive_limit_commute

modified theorem metric.to_inductive_limit_isometry

Modified src/topology/metric_space/gromov_hausdorff.lean

modified def Gromov_Hausdorff.GH_dist

modified theorem Gromov_Hausdorff.GH_dist_eq_Hausdorff_dist

modified theorem Gromov_Hausdorff.GH_dist_le_Hausdorff_dist

modified theorem Gromov_Hausdorff.GH_dist_le_nonempty_compacts_dist

modified theorem Gromov_Hausdorff.GH_dist_le_of_approx_subsets

modified theorem Gromov_Hausdorff.Hausdorff_dist_optimal

modified theorem Gromov_Hausdorff.eq_to_GH_space_iff

modified theorem Gromov_Hausdorff.to_GH_space_eq_to_GH_space_iff_isometric

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

modified def Gromov_Hausdorff.HD

modified theorem Gromov_Hausdorff.HD_below_aux1

modified theorem Gromov_Hausdorff.HD_below_aux2

modified theorem Gromov_Hausdorff.Hausdorff_dist_optimal_le_HD

modified def Gromov_Hausdorff.candidates

modified def Gromov_Hausdorff.candidates_b_dist

modified theorem Gromov_Hausdorff.candidates_b_dist_mem_candidates_b

modified def Gromov_Hausdorff.candidates_b_of_candidates

modified theorem Gromov_Hausdorff.candidates_b_of_candidates_mem

modified theorem Gromov_Hausdorff.isometry_optimal_GH_injl

modified theorem Gromov_Hausdorff.isometry_optimal_GH_injr

modified def Gromov_Hausdorff.optimal_GH_injl

modified def Gromov_Hausdorff.optimal_GH_injr

modified def Gromov_Hausdorff.premetric_optimal_GH_dist