Commit 2022-03-24 05:18 d4e27d0b
View on Github →chore(topology/separation): move a lemma, golf (#12896)
- move
t0_space_of_injective_of_continuousup; - add
embedding.t0_space, use it forsubtype.t0_space.
chore(topology/separation): move a lemma, golf (#12896)
t0_space_of_injective_of_continuous up;embedding.t0_space, use it for subtype.t0_space.