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?

[yhx-12243]

No need to mention T341 and T354 (because it does not directly apply), you can express this next ω step directly (explicitly).

[felixpernegger]

I mean it applies to the subspace (which suffices), but you are right, its simple enough to do it directly.

[yhx-12243]

But this subspace is not fixed (you already done one step), you cannot apply it for a black-box way. So it'd better describe it explicitly. You can refer to existing assertion of P151 of other spaces.

[felixpernegger]

Player 2 picks a neighborhood $U$ of the endpoint $\omega_1$, so he now needs a cover of $X \setminus U$ (and Player 1 implicitly picks covers of $X\setminus U$ because open covers of $X$ restrict to $X \setminus U$). Doesnt matter whether $U$ is fixed, no?
But whatever, I will it down explicitly