Trait Suggestion: 'Countable sigma-product of succesor to first uncountable ordinal' S181 is not Connected P36

[GeoffreySangston]

Trait Suggestion

S000181 is not connected.

Proof/References

The projection $(\omega_1 + 1)^\omega \to \omega_1 + 1$ onto the first coordinate restricts to a surjective continuous map $\sigma(\omega_1 + 1)^\omega \to \omega_1 + 1$.

[GeoffreySangston]

I think it would be better to assert Totally separated actually, as Ordinal Spaces are Totally Separated, and Brian M. Scott shows that products of totally separated spaces are totally separated here.

I haven't changed the title yet just because I wanted to look for any further potential improvements before doing so.