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`.
