Commit 2022-05-23 01:49 56de25ef

chore(topology/separation): golf some proofs (#14279)

• extract minimal_nonempty_closed_eq_singleton out of the proof of is_closed.exists_closed_singleton;
• replace exists_open_singleton_of_open_finset with exists_open_singleton_of_open_finite, extract minimal_nonempty_open_eq_singleton out of its proof.
• add exists_is_open_xor_mem, an alias for t0_space.t0.