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.

[prabau]

How are these three theorems going? Since the theorem ids have been used in the mean time, you should update them to resolve conflicts and then merge main into this PR. Anything you want to discuss further to get this moving?