Commit 2021-03-09 21:43 792e4921

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 Xon s is discrete, then also the topology induces on t is discrete. The proofs are by Patrick Massot.