Commit 2020-02-03 07:14 a3421322

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