feat(topology/metric_space): closed if spaced out (#9754)
If pairwise distances between the points of a set are bounded from below by a positive number, then the set is closed.
Also prove some theorems about `uniform_inducing` and `uniform_embedding` and show that `coe : int → real` is a closed embedding.
