Completing two ordinal(-like) spaces (S36 and S141)

[felixpernegger]

Once #1555 and #1553 are merged, this completes S36 and S141.

[yhx-12243]

Similar as in #1555, I could make a theorem Rothberger (P68) + Ordinal space (P190) implies Countable (P57). The proof I thought of would be: show ω 1 isnt Rothberger (this is done via automatic deduction), then argue that ω 1 + 1 isnt Rotheberger (as I did) and then say that ω 1 + 1 is a closed subset of any other uncountable ordinal space.

This argument is therefore invalid.

[felixpernegger]

Is it fine now? I didnt find strategically rothberger explained anywhere properly, so I hope I understood it properly.

[yhx-12243]

I know what you want to mean, but it is not that “first player is not to pick point, etc.”

The definition is, in 𝑛th round, first player (A) choose an open cover, second player (B) choose one open set from cover. After 𝜔 rounds, if 𝜔 open sets chosen by second player (B) form a cover, then he (B) wins.

You can adapt the trait of S17|P151, very similar.

The proof #1556 (comment) I wrote is just copied from S17|P151.

[prabau]

S36 | P151: Sorry, but this does not make sense. This does not seem related to the "game" for Strategically Rothberger. In that game, Player 1 chooses an open cover, then Player 2 chooses a member of that cover. Etc.

Added later: @yhx-12243 already addressed this above.

[prabau]

S141 | P103: the subspace omega_1 + 1 is actually closed. I think you meant to use omega_1.

[felixpernegger]

Sorry this is really embarrassing. I hope is it good now?