search

pi-base / data

A community database of topological counterexamples
https://topology.pi-base.org/
Creative Commons Attribution 4.0 International
69 stars 24 forks source link

Theorem Suggestion: Weakly Countably Compact + LOTS => sequentially compact #639

Closed Jianing-Song closed 2 months ago

Jianing-Song commented 2 months ago

Weakly Countably Compact + LOTS => sequentially compact

Note that we have Weakly Countably Compact + T_1 => countable compact (T19), so Weakly Countably Compact + LOTS => countably compact. As said in the preceeding issue, Countably Compact = Every sequence has a limit point (every neighborhood contains infinitely many terms).

It is standard that every sequence in LOTS has a monotone subsequence, so by countable compactness it has a limit point. A limit point of a monotone sequence is just the limit, so we've just found a converging subsequence.

This shows that for LOTS, countable compactness and sequential compactness are equivalent (even without first-countability which fails for every ordinal number $>\omega_1$), and thus there is no compact LOTS which is not sequentially compact (in contrast to $\omega_1$ being non-compact but sequentially compact).

prabau commented 2 months ago

Good observations. We should add that.

Since countably compact and weakly countably compact are equivalent for T1 spaces (already known by pi-base), I think it would be more natural to use the equivalent version [countably compact + LOTS ==> sequentially compact].

prabau commented 2 months ago

Fine for now, but in general it's better not to close issues until they have been resolved, i.e., until any corresponding PR have been merged. I'll review the PR today.

Jianing-Song commented 2 months ago

Fine for now, but in general it's better not to close issues until they have been resolved, i.e., until any corresponding PR have been merged. I'll review the PR today.

Thanks for the reminder. I still have doubt about keeping or deleting S36/P20. What's your opinion regarding the other files mentioned in that PR?

prabau commented 2 months ago

I still have doubt about keeping or deleting S36/P20.

Deleting in this case is the right thing to do (already expanded in comments to the PR). Note that this will not break anything for pi-base users. https://topology.pi-base.org/spaces/S000036/properties/P000020 will always have something informative (either the previous manual justification, or the new deduction based on theorems).

Jianing-Song commented 2 months ago

I still have doubt about keeping or deleting S36/P20.

Deleting in this case is the right thing to do (already expanded in comments to the PR). Note that this will not break anything for pi-base users. https://topology.pi-base.org/spaces/S000036/properties/P000020 will always have something informative (either the previous manual justification, or the new deduction based on theorems).

Ah sorry I didn't see the comment there, my bad (perhaps due to forgetting to refresh the page)