Theorem Suggestion: countable + metrizable => LOTS

Theorem Suggestion

If a space is:

countable P57
metrizable P53

then it is orderable P133.

Analogous theorem works for the local properties: P93 + P82 $\Rightarrow$ P120

Rationale

This theorems would demonstrate that no spaces satisfy the following searches:

https://topology.pi-base.org/spaces?q=countable%2BMetrizable%2B%7ELOTS
https://topology.pi-base.org/spaces?q=locally+countable%2Blocally+Metrizable%2B%7ELocally+orderable

References

See Corollary 6.2.8. and Excercise 6.3.2.f in Engelking.

Remark

It could be also decomposed upon adding strongly 0-dimensional property (see #1388) into

countable + regular $\Rightarrow$ strongly 0-dim
metrizable + strongly 0-dim $\Rightarrow$ LOTS

I have no idea if there is any meaningful decomposition for the local version.

Strongly 0-dimensional doesn't work that well for subspaces, but it's closed under closed subspaces, so we could have
regular + strongly 0-dimensional + locally metrizable => locally orderable perhaps

I definitely agree we should add strongly 0-dimensional first

Theorems planned to be added:

P53 + P217 $\Rightarrow$ P133 ("global")
P82 + P93 $\Rightarrow$ P120 ("local")

Would there be an advantage in releasing one and then the other separately, so one could see what additional examples are not covered by the first theorem alone?
(or at least do a first commit with one theorem, check which traits are missing without the second one, then do another commit)

See the branch pzjp/order-thm. Herrlich uses different definition of strongly 0-dimensional (and his paper is in German) so I used Engelking's excercise as a refernce but simplified the construction-hint a bit.
Unfortunatley the branch was created (a moment) before you've merged locally-ordered-4 and P133 for S102 is missing (I redirect to this proof for a hint on the constructed order topology).

You can always merge main into your branch.

Should there be also a cleanup? For some spaces asserting P133 or P120 it became derivable.

The cleanup can be done at the same time in this case.

See the branch pzjp/order-thm. Herrlich uses different definition of strongly 0-dimensional (and his paper is in German) so I used Engelking's excercise as a refernce but simplified the construction-hint a bit. Unfortunatley the branch was created (a moment) before you've merged locally-ordered-4 and P133 for S102 is missing (I redirect to this proof for a hint on the constructed order topology).

The Engelking exercise does not appear trivial. If it's a little involved, it's preferable to give details in a mathse post for example (or find a more detailed reference). If you go that route, as usual either do question and answer yourself (properly motivated to avoid downvotes from some people), or ask one of us to post a question.

Maybe someone else should ask the question in that case. I'm not that confident about the details of my approach (but if it works it is a bit easier than the hint in Engelking).

I'll take a closer look at the proof you have in T771 (in #1421) first. Maybe it's not that bad and there is no need to ask on mathse.

Navigation Menu

Repository navigation

Theorem Suggestion: countable + metrizable => LOTS #1413