mathlib3
3055b3c0 - chore(topology/metric_space/isometry): rename `(e)metric.isometry.diam_image` to `isometry.(e)diam_image` (#2073)

Commit
5 years ago
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`. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading