Space: $\mathbb{R} \times \omega$

[JSMassmann]

It's a pretty simple space, so @Moniker1998 advised I just submit a PR without an Issue.
It answers a search that currently has no results, namely Polish + homogeneous + ~connected + ~totally disconnected.
It's also P41, P120 and P184, but I didn't want to overwhelm with so many traits in one PR.

[prabau]

observation: $X$ is homeomorphic (for example) to the closed subspace $\mathbb R\times\mathbb Z$ of $\mathbb R^2$. (useful also to show X is embeddable in some Euclidean space)

Possibly worth mentioning later, if we find this useful. For example, it could an alternative way to show that X is Polish.

But both that way and the current justification that X is Polish (P116) rely on some meta-property that is currently not in pi-base and that need to be added to P116. This should be done in the same PR since we are making use of it. (for products and for closed sets in particular -- see https://github.com/pi-base/data/wiki - "Conventions and Style" for usual wording.)

I have not checked the other properties, but please take a look if other meta-properties are missing.

[Moniker1998]

Suggested change

	$\{(n, n + 1) \times \omega: n \in \mathbb{Z}\}$ is an open cover with no finite subcover.
	$X$ contains {S25} as a closed subspace and {S25|P16}.

[Moniker1998]

Suggested change

	$[n, n + 1] \times \{m\}$ is compact for all $n, m \in \mathbb{N}$, and the union of all of these is the whole space.
	Product of {P17} spaces

[Moniker1998]

Also, add meta-property that P17 is closed under countable products

[Moniker1998]

Suggested change

	Since {S25|P36}, $\mathbb{R} \times \{n\}$ is a connected component for each $n \in \mathbb{N}$.
	Has {S25} as a subspace and {S25|P47}

[prabau]

If we want to rely on a meta-property for P47, we should instead claim {S25|P47} (which expands to X not being totally disconnected).

But maybe just easier, just say $\mathbb R\times\{0\}$ is a connected subspace with more than one point.
(which is closer that what @JSMassmann had initially).

[Moniker1998]

Suggested change

	For any $A \subseteq \omega$, $\mathbb{R} \times A$ is clopen since we give $\omega$ the discrete topology.
	Product of {S25} and {S2}, and {S2|P36}

[prabau]

Again, that relies on meta-properties that are missing from pi-base.
On the other had, what @JSMassmann had initially is more than we need.

How about just saying:
$\mathbb R\times\{0\}$ is a nonempty proper clopen subset of $X$. ?
(more justification not needed as it's obvious)

[Moniker1998]

@prabau I've already mentioned that in the other comment. And adding the metaproperty is useful, and easier

[Moniker1998]

Need to add metaproperty

[Moniker1998]

@JSMassmann I've made it so that the justifications use metaproperties instead of writing things explicitly. @prabau can check for stylystic choices

[JSMassmann]

Sorry that I haven't written a reply yet, I'm a bit busy. I'm not sure what I should do wrt the metaproperties, since as @prabau pointed out many of them aren't in pi-base yet.

[Moniker1998]

@JSMassmann just two of them