feat(topology/separation): add t2_space_iff (#12628)
feat(topology/separation): add t2_space_iff (#12628)

From my formalising mathematics 22 course





leanprover-community/mathlib,leanprover-community/mathlib