mathlib

d4e27d0b - chore(topology/separation): move a lemma, golf (#12896)

chore(topology/separation): move a lemma, golf (#12896) * move `t0_space_of_injective_of_continuous` up; * add `embedding.t0_space`, use it for `subtype.t0_space`.