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

	Since {S25|P36}, $\mathbb{R} \times \{n\}$ is a connected component for each $n \in \mathbb{N}$.
	$X$ contains a copy of {S25} 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).

[prabau]

$X$ contains a copy of {S25} and {S25|P47}.

[Moniker1998]

@prabau feel free to edit

[prabau]

edited the suggestion

[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

[prabau]

@JSMassmann @Moniker1998 Something along the lines of Moniker's suggestion should be ok.
P36 (connected) has the meta-property
"An arbitrary product of nonempty spaces satisfies this property iff each of its factors does".
So if one of the factors is not connected (and the space is nonempty, which is the case here), neither is the product space.

So I think the following should be good:
{S2|P36}, hence neither is the product $\mathbb R\times\omega$.

or even just {S2|P36}. ?

What do you think?

[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

[prabau]

I have added some relevant meta-properties. Please review that.

Note: $\sigma$-compact (P17) is preserved by finite products, but not by countable products:
https://topology.pi-base.org/spaces/S000030/properties/P000017

[JSMassmann]

Okay, the metaproperties look good. The last question is what to do with P36 and P47, I guess.

[prabau]

Suggested change

	{S2|P116} and {S25|P116}, hence so is their product.
	{S25|P116} and {S2|P116}, hence so is their product.

swap the factors so it matches the order in the space name
(easier to see in preview mode)

[prabau]

@JSMassmann Two remaining things:

• Space: $\mathbb{R} \times \omega$ #1845 (comment)
• Space: $\mathbb{R} \times \omega$ #1845 (comment)

What do you think?