A bunch of new theorems

[Jianing-Song]

Hi everyone, I will be soon back from summer holiday, and I would like to add the following theorems:

$\bullet$ ~empty + completely metrizable + ~has an isolated point $\Rightarrow$ ~cardinality $< \mathfrak{c}$: You can see https://math.stackexchange.com/a/2304598 or https://mathoverflow.net/questions/22830/improvements-of-the-baire-category-theorem-under-not-ch for a proof.

$\bullet$ Sequentially discrete + Sequentially Compact $\Rightarrow$ finite: Quite obvious.

$\bullet$ LOTS + Connected $\Rightarrow$ Locally connected: The convex sets (including open intervals) of a connected LOTS are connected.

$\bullet$ LOTS + Path Connected $\Rightarrow$ Locally path connected: The convex sets (including open intervals) of a path-connected LOTS are path-connected. I believe that the fact should be as fundamental as the one above, but I couldn't find it directly on the Internet, so I'm writing it out: Suppose that we want to join $a < b$ by a path in a convex subset of a path-connected LOTS $X$. There is one path $\gamma$ in $X$. Define $t_0=\sup\{t\in[0,1]:\gamma(t)\le a\}$ and $t_1=\inf\{t\in[0,1]:\gamma(t)\ge b\}$, then by intermediate value theorem we must have $\gamma(t_0)=a$ and $\gamma(t_1)=b$. By definition $\gamma(t)\in[a,b]$ for $t\in[t_0,t_1]$, so we have found a path joining $a$ and $b$ in $[a,b]$.

$\bullet$ GO space + Locally Connected $\Rightarrow$ Weakly locally compact: Every point has a connected open neighborhood $U$ which is a connected LOTS by {T131}, and every closed interval of $U$ with respect to the order on $U$ giving the order topology is compact (see https://en.wikipedia.org/wiki/Total_order#Completeness).

$\bullet$ GO space + sequentially discrete $\Rightarrow$ anticompact: Let $Y$ be a compact subset of a GO space $X$, then $Y$ is a compact LOTS by {T125}, so it is sequentially compact by {T488}, then finite by sequential discreteness of $X$.

$\bullet$ GO space + ~totally disconnected $\Rightarrow$ ~anticompact (in fact, has compact subsets of cardinality $\ge\mathfrak{c}$): Let $Y$ be a nontrivial connected subset of a GO space $X$, then $Y$ is a connected LOTS by {T131}, meaning that every closed interval of $Y$ with respect to the order on $Y$ giving the order topology is compact, and those nontrivial intervals have cardinality $\ge\mathfrak{c}$ as any nontrivial connected $T_4$ space does.

$\bullet$ GO space + extremally disconnected $\Rightarrow$ discrete: See https://math.stackexchange.com/q/4913523/1039170. The answer proofs for LOTS but the proof generalizes easily for GO-spaces as remarked in the original question.

How do you think of these theorems? Please don't hesitate to share your concerns! Thank you in advance.

[prabau]

This is great! I have not looked in detail, but any result that was not previously derivable is a good addition to pi-base. Even better if the new result allows to derive new traits for some spaces, or to remove some redundant traits or strengthen previous results for example. I'd say just go for it and create some PRs, so each result can be analyzed and discussed.

One recommendation. Please do not create one huge PR with all the results. Instead, you can start creating some PR, one result at a time (or maybe more than one if two results are closely linked and need to be discussed together). That will make it easier to review and get things approved. If there are dependencies between results, it may be even better to wait until each PR is approved before starting the next one, so we can better see the dependencies when playing with it in the database. If each PR is short, we should be able to get to it quickly.

Also the usual guideline. Proofs that are short and pretty straightforward can be written directly in pi-base as justification. But anything more involved should refer to some post on mathse (or to something in books or the published literature of course).

[StevenClontz]

Please do not create one huge PR with all the results. Instead, you can start creating some PR, one result at a time

💯 👆

Looking forward to your contributions @Jianing-Song :-D