Stream: Is there code for X?
Adam Topaz (Nov 24 2020 at 23:01):
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
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 (Nov 24 2020 at 23:18):
I think I must have proved this at some point, but maybe it was slightly different...
Adam Topaz (Nov 24 2020 at 23:21):
I didn't find anything in the
topology.separation file. Is there another file where this might be?
Reid Barton (Nov 24 2020 at 23:26):
I guess I'm confusing it with slightly different things
Adam Topaz (Nov 25 2020 at 15:31):
Last updated: May 16 2021 at 05:21 UTC