Allow empty Strongly Choquet spaces

[StevenClontz]

This is something that became clear when toying around with #1676 (which is purely exploratory, for the purpose of helping conversation at STDC).

In addition to cleaning up several theorems by allowing the empty space to be strongly Choquet, it seems clear by the definition that Player 1 is the player that loses the Choquet game on an empty space, because Player 1 has no legal moves.

This also makes us less likely to make "trivial" mistakes down the road, as often the empty case is ignored. (E.g. I kept hitting contradictions when experimenting with subcompactness in the toy PR, because I didn't specifiy nonempty.)

[StevenClontz]

Choquet theorems before:

Choquet theorems after:

[mathmaster13]

Why were they made nonempty in the first place?

[prabau]

I am not sure we can say the empty space is "technically strongly Choquet" just from the stated definition.

Looking at it differently, for Player 2 to win, it needs to force a certain sequence of nested open sets $U_n$ such that their intersection is nonempty. But if one starts with an empty space, one can never get the intersection of anything to be nonempty. In that sense, one could say that Player 2 can never win.

But more reasonably, it seems to me that the game itself does not ever get off the ground if $X$ is empty. Player 1 is blocked at the first move like you said. That does not mean that Player 1 loses the game, just that the game does not make sense in that case. There is no winner or loser. There is just no game at all.

Could we maybe declare by fiat that the empty space is P206? What do you think?

[yhx-12243]

After this PR T290 is redundant that can be removed.

[prabau]

@StevenClontz Regarding #1677 (comment), is it possible after all that one could understand what "technically strongly Choquet" means based on a certain formalization of the game and of what a strategy for the game is? And in that formalization it would indeed be the case that the empty space is strongly Choquet?

But how would you formalize exactly the notion of strategy for P2 and the notion that P2 wins the game?