mathlib

3166f4ef - feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523)

feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523) These lemmas form part of a simplification of the proofs of #5361. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>