Add equivalence of countable compactness using sequences, and Countably Compact + LOTS => Sequentially compact

[Jianing-Song]

As described in issues #638 and #639. I deteleted S000036/P000020.md, since it is no more needed to verify by hand that $\omega_1+1$ is sequentially compact. Please kindly correct me if this is inappropriate (perhaps we still need this file for a backup). Thanks!

[Jianing-Song]

By the way, S20/P27, S33/P27 and S34/P27 ($\omega+1$, $\omega\cdot 2$ and $\omega\cdot 2+1$ are second countable) are not needed: the system already has enough information to show LOTS + countable => second countable.

Likewise for S36/P29 ($\omega_1+1$ does not satisfy countable chain condition): we have LOTS + CCC => first countable.

For S35/P28 ($\omega_1$ is first countable): we know that $\omega_1$ is locally countable, and LOTS + countably tight => first countable.

And also for S35/P49 ($\omega_1$ is not extremally disconnected), as $\omega_1$ is not sequentially discrete and we have T10.

Do we delete or keep them?

[prabau]

Made some minor tweaks. Please let me know how it looks and I'll approve/merge.

@StevenClontz Can you comment on the following?

As far as removing redundant trait files, it's a good idea to do so, especially when the justification was just referring to the "General Reference Chart" from Steen & Seebach. That's one of the side benefits of adding theorems.

Maybe in some cases, the justification in a trait file was pointing to a specific item for a space in S&S that could be interesting. But if this can deduced instead, I would say it's generally ok to delete it. Most of the time, the deduction from theorems in pi-base is equally informative. An interested user can always check S&S by themselves if they want to. (Possibly one case where it could make a difference is when a trait deduction from theorems would use a long chain of theorems, but S&S would have a more direct and simpler justification?)

If Steven is ok with that, I think after this PR is merged you can do another one to remove all the redundant traits as suggested.

[Jianing-Song]

Made some minor tweaks. Please let me know how it looks and I'll approve/merge.

@StevenClontz Can you comment on the following?

As far as removing redundant trait files, it's a good idea to do so, especially when the justification was just referring to the "General Reference Chart" from Steen & Seebach. That's one of the side benefits of adding theorems.

Maybe in some cases, the justification in a trait file was pointing to a specific item for a space in S&S that could be interesting. But if this can deduced instead, I would say it's generally ok to delete it. Most of the time, the deduction from theorems in pi-base is equally informative. An interested user can always check S&S by themselves if they want to. (Possibly one case where it could make a difference is when a trait deduction from theorems would use a long chain of theorems, but S&S would have a more direct and simpler justification?)

If Steven is ok with that, I think after this PR is merged you can do another one to remove all the redundant traits as suggested.

Thanks for your reply. I am OK with your changes. Thanks a lot for making them.

In my opinion, the automatic deduction is already easy enough for the redundant proofs listed other than S36/P29. But the proof of S36/P29 would become the general case Well-orderable + countable chain condition => countable after we add the property ordinal space in the database.

If all of you agree, I would delete these files when adding the property ordinal space.

[prabau]

Sounds like a good plan. Approving this in the mean time.

For general guideline, hope @StevenClontz can still comment on the above .

[Jianing-Song]

By the way, S20/P27, S33/P27 and S34/P27 (ω+1, ω⋅2 and ω⋅2+1 are second countable) are not needed: the system already has enough information to show LOTS + countable => second countable.

Likewise for S36/P29 (ω1+1 does not satisfy countable chain condition): we have LOTS + CCC => first countable.

For S35/P28 (ω1 is first countable): we know that ω1 is locally countable, and LOTS + countably tight => first countable.

And also for S35/P49 (ω1 is not extremally disconnected), as ω1 is not sequentially discrete and we have T10.

Do we delete or keep them?

@StevenClontz Would you agree with me to delete these files? If so, I will perform these edits recently :)

[StevenClontz]

Finally catching up on email after running a workshop last week...

I prefer less assertions in the pi-Base, and reling on automated deduction wherever possible. So please go ahead and remove any space-property pairs that can be deduced from theorems.