mathlib

22b61b26 - feat(topology/subset_properties): separated of discrete (#4952)

feat(topology/subset_properties): separated of discrete (#4952) As [requested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/totally.20disconnected.20of.20discrete/near/216021581).