More stuff on finitely many open sets

[artemetra]

This is a work-in-progress PR meant to address more comments in #1800.

[artemetra]

Hm something's wrong with the website for me, it seems like this broke deduction rules somehow? What happened?

[prabau]

Feel free to mark this as draft until it's ready to review.

[felixpernegger]

@artemetra generally these issues resolve by clearing cookies

[yhx-12243]

@‍artemetra generally these issues resolve by clearing cookies

e.g., click Reset in advanced pages

[artemetra]

I tried reset button, clearing cookies, using incognito, using a different browser and a different computer and I still get the same behavior :(

[artemetra]

This seems really odd tho, did it arrive at a contradiction? I'll reread the comments in the issue thread soon to make sure I copied it correctly

[artemetra]

Okay yeah for some reason I wrote a contradictory result, it works now.

[prabau]

Hmm, this is getting kind of long. Usually we prefer not to add a new space at the same time as a bunch of new theorems, unless there is a specific reason to do so?

[artemetra]

@prabau That's fair, I added it more to test the theorems we are adding here and seeing what else can be derived from Has finitely many open sets. I removed the space now and I'll make a separate PR for it (from branch artem/s227) when I am done with this one.