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?

[artemetra]

I kinda forgot about this but I hope to get it done today! Currently writing the proof for Sober + Alexandrov => Scattered. I'll reindex the theorems accordingly.

[artemetra]

@prabau should be ready for review now, comments are welcome

[prabau]

Great. I'll check this later today.

[prabau]

T931: This is a little too wordy and can be written in a clearer way, letting pi-base do part of the work. See suggestion below, using "(Explore)" links.

Note however that this relies on the appropriate meta-properties for the properties involved. So need to add Kolmogorov quotient meta-prop for Noetherian.

[prabau]

T930: Nice proof.

Minor stuff: BWOC: It's preferable not to use abbreviations that most people will not be familiar with.

[prabau]

T929 sober + Alexandrov => scattered : Hmm, a little long and lots of notation there. I assume this is based on the chatGPT link. I am wondering if things could be expressed in a shorter way. Or maybe better, since is involves notions that would be of interest to a general audience, this would be better in a mathse post. One of us could ask over there and you could answer (or wait for other answers first for variety?).
What do you think?

[artemetra]

@prabau yes, this is largely based on ChatGPT's proof, with some unnecessary parts pruned and some parts elaborated on more (where I felt it wasn't justified enough). The notation paragraph I copied from T927, maybe the notation can be included as part of the Alexandrov property description instead..

As for mathse idea: I don't object to it, but I'll try to find some ways to shorten the proof first. As it looks right now I think some notions can be simplified (for example i am not 100% sure we need to fully introduce directed lower sets).

[prabau]

Note: the above relies on the fact that in a hyperconnected space no two points can be separated by disjoint neighbourhoods. (That's one of the characterizations listed in https://en.wikipedia.org/wiki/Hyperconnected_space.)

Would that be useful to add to https://topology.pi-base.org/properties/P000039? Or too simple to add?

[artemetra]

Note: the above relies on the fact that in a hyperconnected space no two points can be separated by disjoint neighbourhoods.

Doesn't this follow immediately from "no two nonempty open sets are disjoint"?