Update S77 (Michael's product topology)

[yhx-12243]

See #1704 (comment).

[prabau]

I think this would be a good opportunity to change the name to a better one. "Michael's product topology" is not very descriptive. We could change it to "Product of Michael line and irrational numbers".
(and make the previous name an alias).

What do you think?

[prabau]

I have not given it any thought, but just to be thorough, why is an arbitrary product of strongly Choquet space strongly Choquet?

[prabau]

P61: what it the argument here? If a product $X\times Y$ is cozero complemented, why are $X$ and $Y$ the same?

Maybe it is not so trivial. I may replace it with assertion of P62, which is directly to factors.

[prabau]

Just to make sure this was not prematurely approved.
@felixpernegger FYI

[yhx-12243]

I have not given it any thought, but just to be thorough, why is an arbitrary product of strongly Choquet space strongly Choquet?

Just play each dimension indepenently, (ref: 8.16(ii) in zb:0819.04002)

[prabau]

Yes, I can see how that works, using basic open sets for the product topology.