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`.
