More traits for S220 S221 Right ray topologies on omega_1

[prabau]

This adds most remaining decidable traits for S220 (Right "closed ray" topology on $\omega_1$) and S221 (Right "open ray" topology on $\omega_1$).

S221-P230 (locally simply connected): The justification is a general theorem [Hereditarily connected => Locally simply connected]. I did not add it as a new theorem because once we add the "locally contractible" property, we can have a stronger result with that.

The remaining traits I am not sure about are:

• (P38) injectively path connected
• (P43) locally injectively path connected

(obviously false if (CH) is false, but could be false in general)

[GeoffreySangston]

I checked each proof and checked the reference. Everything looked good to me.

[felixpernegger]

I checked each proof and checked the reference. Everything looked good to me.

If you did this, I recommend you click "Approve". :)

[GeoffreySangston]

@prabau Hmm I accidentally did it out of order (hitting approve before your final change). I'll see how to fix it.

[prabau]

If anyone has an idea about "injectively path connected", that would be great. Can be added later.

[GeoffreySangston]

Re-do Approve.

[prabau]

@prabau Hmm I accidentally did it out of order (hitting approve before your final change). I'll see how to fix it.

That's irrelevant. It remains approved, unless you "request rereview" with a button at the top I think?

[GeoffreySangston]

@prabau Well clearly I'm botching this. My apologies. I don't think I ever did the "Enable auto-merge (squash)" steps now that I think about it. Maybe that's why I'm confused?

[prabau]

??? @GeoffreySangston you have to click on the Approve button from the Files changed page ("Submit review").

[GeoffreySangston]

??? @GeoffreySangston you have to click on the Approve button from the Files changed page ("Submit review").

I assure you I've done this.

Edit: Well, maybe I submitted it from a different page.

[prabau]

Now if you want to do "squash and merge", remember to blank out the detailed description before clicking.

[felixpernegger]

If anyone has an idea about "injectively path connected", that would be great. Can be added later.

Does this work?:

Let f:[0,1] -> X be an injective map. Note the image of f has to be unbounded because of cardinality.
Take some countable, dense subset E of [0,1] (rational numbers i.e.), then f(E) is countable and thus bounded by say u. But then $(u+1, \infty)$ must have open preimage, but since E is dense, the preimage is empty, contradiction with f unbounded

[GeoffreySangston]

I think @felixpernegger's argument applies verbatim to the locally injectively path connected trait of S221 as well.

[prabau]

Very nice. Another way, maybe easier, to rewrite the argument: f(E) is countable and thus bounded by say $u\in\omega_1$. So $f(E)$ is contained in the closed set $[0,u]$. And by density of E in $[0,1]$, $f([0,1])$ is also contained in $[0,u]$. Since $[0,u]$ is countable, $f$ cannot be injective.