Commit 2020-03-02 12:33 3055b3c0

View on Github →

chore(topology/metric_space/isometry): rename (e)metric.isometry.diam_image to isometry.(e)diam_image (#2073) This way we can use dot notation to access these lemmas. Also add (e)diam_range.

Estimated changes

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/metric_space/isometry.lean

deleted theorem emetric.isometry.diam_image

added theorem isometry.diam_image

added theorem isometry.diam_range

added theorem isometry.ediam_image

added theorem isometry.ediam_range

deleted theorem metric.isometry.diam_image