t2_space instances for disjoint union

Stream: Is there code for X?

[Adam Topaz]

I don't think mathlib has t2_space instances for disjoint unions, or at least I couldn't find them, even with the help of apply_instance.
I added them in the following branch#t2_sums
Assuming they actually don't exist yet, I will open a PR soon (after some additional cleanup)

[Reid Barton]

I think I must have proved this at some point, but maybe it was slightly different...

[Adam Topaz]

I didn't find anything in the topology.separation file. Is there another file where this might be?

[Reid Barton]

I guess I'm confusing it with slightly different things

[Adam Topaz]

#5113