mathlib3

a3421322 - refactor(topology/metric_space/emetric_space): redefine `diam` (#1941)

refactor(topology/metric_space/emetric_space): redefine `diam` (#1941) * feat(data/set/basic): define `set.subsingleton` Also rename `nonempty.of_subset` to `nonempty.mono` * Add a missing lemma * refactor(topology/metric_space/emetric_space): redefine `diam` * Give a more readable definition of `emetric.diam`; * Add a few lemmas including diameter of a pair and of a triple of points; * Simplify some proofs; * Reformulate some theorems to use `∀ (x ∈ s) (y ∈ s)` instead of `∀ x y ∈ s` because the former plays better with existing `simp` lemmas. * Redefine `set.subsingleton` using `(x ∈ s) (y ∈ s)`, prove `metric.diam_triangle`