S181 is not connected

[felixpernegger]

also added useful metaproperty for p36 (for the proof one can argue similarly as in the finite case)

[Moniker1998]

Should this meta-property be written down for the wiki? @prabau

[prabau]

Let me think about the best way to phrase this.

[prabau]

Comparing with Willard Thm 26.10:
"A nonempty product space is connected iff each factor space is connected."

Note that "nonempty product" (i.e., the product itself is nonempty) is equivalent to each factor being nonempty. Also, "product space" is used here for an arbitrary product.

Engelking 6.1.15 has something more wordy and more explicit.

---

So here are a few alternatives:

(1) "An arbitrary product of nonempty spaces satisfies this property iff each of its factors does."

(2) "A nonempty arbitrary product $\prod_i X_i$ satisfies this property iff each $X_i$ does."

(3) Keeping the two implications separate:
(3.1) "This property is preserved by arbitrary products."
(3.2) "If a nonempty product $\prod_i X_i$ satisfies the property, so does each $X_i$."

(3.1) is formulation we already use elsewhere.
(3.2) does not need to specify arbitrary products. Because the implication (3.2) only goes in one direction, the result is enough for product of two spaces. Any factor in $X=\prod_i X_i$ is also a factor of $X$ viewed as a product of two spaces, so it also holds for arbitrary products. So it's the same thing either way.

I kind of like (2).

@felixpernegger @Moniker1998 What do you think?

[felixpernegger]

both is fine, whatever

[Moniker1998]

@prabau

I like (1) and (3.1). I find (3.2) okayish, but I would prefer a version with no symbols. And I dislike (2) (because of the word arbitrary).

[felixpernegger]

@prabau

I like (1) and (3.1). I find (3.2) okayish, but I would prefer a version with no symbols. And I dislike (2) (because of the word arbitrary).

This PR uses the other direction of the "iff" from (1) explicitly

[prabau]

The word "arbitrary" is not used for this PR, but it's needed to get the other implication (i.e. "preserved by arbitrary products"), which is useful to have in general.

What would you think of having both implications separately and without symbols?
(3.1) "This property is preserved by arbitrary products."
(3.2') "If a nonempty product space satisfies this property, so does each of its factors."

[felixpernegger]

The word "arbitrary" is not used for this PR, but it's needed to get the other implication (i.e. "preserved by arbitrary products"), which is useful to have in general.

What would you think of having both implications separately and without symbols?
(3.1) "This property is preserved by arbitrary products."
(3.2') "If a nonempty product space satisfies this property, so does each of its factors."

im not in favour of omitting "arbitrary". Yes from finite one can deduce arbitrary anyways, but why not be clear in the first place.

[prabau]

@felixpernegger Note that (3.2') did not say "finite product", just "product" in general.

@Moniker1998 what do you think of (3.1), (3.2') and the other choices?

[felixpernegger]

this is what i meant

[felixpernegger]

Why can't we just use the metaproperty the way I wrote it? I dont quite understand the issue at hanf

[prabau]

Moniker does not like the word "arbitrary". So let's see what his thinking is.

[Moniker1998]

Moniker does not like the word "arbitrary". So let's see what his thinking is.

Actually I believe my problem is with the word order, rather than the word "arbitrary" itself.
I had a feeling something is wrong, but maybe I described that feeling poorly.

[Moniker1998]

Why can't we just use the metaproperty the way I wrote it? I dont quite understand the issue at hanf

I like the way you wrote it, and as long as it's made standard I am willing to accept it.

[prabau]

Note: we already had a different phrasing for that meta-property for https://topology.pi-base.org/properties/P000062 (already merged). But that was only one implication, not iff.

We can go with your suggestion for now. Feel free to approve and merge, and add to the wiki.

[Moniker1998]

Note: we already had a different phrasing for that meta-property for https://topology.pi-base.org/properties/P000062 (already merged). But that was only one implication, not iff.

We can go with your suggestion for now. Feel free to approve and merge, and add to the wiki.

I don't think that phrasing is good. "Nonempty product space"? That sounds strange. @prabau

[prabau]

@Moniker1998 I assume your comment is about what's used for P62?

"nonempty product space" seems fine to me. It is exactly the terminology used by Willard for example (see #1716 (comment)).
"Product space" means a space that can be written as a product of a family of spaces, i.e., $X$ is homeomorphic to some $\prod_{i\in I} X_i$. And the product is nonempty exactly when each $X_i$ is nonempty.
So "nonempty product space" is an equivalent way of saying "product of nonempty spaces".

If you want to rephrase the P62 metaprop to be closer to Felix's version, that's fine with me. Something like:
"If a product of nonempty spaces satisfies the property, so does each of its factors."

[Moniker1998]

@prabau yes I was talking about that. And just because Willard says it doesn't mean it's not a strange phrasing.
If we want to use it we should abandon the "space". Just say non-empty product.