Commit 2021-03-27 15:21 d1044139

chore(topology/metric_space): golf, generalize, rename (#6849)

Second countable topology

• generalize metric.second_countable_of_almost_dense_set to a pseudo emetric space, see emetric.subset_countable_closure_of_almost_dense_set (for sets) and emetric.second_countable_of_almost_dense_set (for the whole space);
• use it to generalize emetric.countable_closure_of_compact to a pseudo emetric space (replacing closure t = s with s ⊆ closure t) and prove that a sigma compact pseudo emetric space has second countable topology;
• generalize second_countable_of_proper to a pseudo metric space;

emetric.diam

• rename emetric.diam_le_iff_forall_edist_le to emetric.diam_le_iff;
• rename emetric.diam_le_of_forall_edist_le to emetric.diam_le.