Commit 2021-10-18 08:19 fb5c0bec

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.