Locally orderable has the alpha properties

[felixpernegger]

Gives 8*5=40 new traits!
https://topology.pi-base.org/spaces?q=locally+orderable+%2B+%3F%24%5Calpha_1%24

Since cozero complemented was finished for LOTS by @prabau, it seems plausible to feasable to complete all LOTS (excpet maybe the Luzin sets and some others)

[prabau]

Since cozero complemented was finished for LOTS by @prabau,

For the record, I added cozero complemented for many spaces, but did not finish them all. There are more that should be added. Anyone, feel free to have a go at it. I may do some more later, but no time now.

[prabau]

Wait, you meant for LOTS. For LOTS I did complete it.

[prabau]

Related to this result, each $\alpha_i$ property is hereditary (check me on this).
So it would also follow that GO-spaces have the alpha_i properties. We could add this as another theorem.

(Side remark: That does not follow from the proposed theorem. It would follow from the notion of "locally GO-space", but I think we should NOT introduce that notion. It's too artificial and not really used in the literature I think.)

[prabau]

(not directly relevant, but kind of background for the proof: https://topology.pi-base.org/theorems/T000236)

[felixpernegger]

Good point. At least we would not get any new traits from adding the GO space theorem,
https://topology.pi-base.org/spaces?q=GO-space+%2B+%7Elocally+order+%2B+%7ECountably+tight

[felixpernegger]

I added a sketch of the general case now on MSE.

[felixpernegger]

I added a theorem for GO-spaces now.

[Moniker1998]

@felixpernegger did you look at how I modified your post?

[prabau]

@felixpernegger did not say it explicitly, but I was hoping you would add the hereditary meta-property for all the alpha_i.
Since the PR is already approved, let me add this separately.

[Moniker1998]

@prabau oh I thought this was already added

[Moniker1998]

@prabau are you sure? To me the metaproperty is there

[Moniker1998]

#1552 it was added in this PR

[prabau]

@Moniker1998 Thanks for adding it. I was looking at an older branch.