Zulip Chat Archive

Stream: Is there code for X?

Topic: t2_space instances for disjoint union


view this post on Zulip 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 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)

view this post on Zulip Reid Barton (Nov 24 2020 at 23:18):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 24 2020 at 23:26):

I guess I'm confusing it with slightly different things

view this post on Zulip Adam Topaz (Nov 25 2020 at 15:31):

#5113


Last updated: May 16 2021 at 05:21 UTC