mathlib

d04fff95 - feat(topology/{order,separation}): several lemmas from an old branch (#12794)

feat(topology/{order,separation}): several lemmas from an old branch (#12794) * add `mem_nhds_discrete`; * replace the proof of `is_open_implies_is_open_iff` by `iff.rfl`; * add lemmas about `separated`.