Commit 2022-03-18 21:54 d04fff95

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.