mathlib

792e4921 - feat(topology/separation): add API for interaction between discrete topology and subsets (#6570)

feat(topology/separation): add API for interaction between discrete topology and subsets (#6570) The final result: Let `s, t ⊆ X` be two subsets of a topological space `X`. If `t ⊆ s` and the topology induced by `X`on `s` is discrete, then also the topology induces on `t` is discrete. The proofs are by Patrick Massot.