Theorem Suggestion: perfectly normal LOTS are first countable

[pzjp]

Theorem Suggestion

If a space is:

• Orderable P133
• Perfectly normal P15

then it is First countable P28.

Rationale

This theorem would demonstrate that no spaces satisfy the following search:
https://topology.pi-base.org/spaces?q=LOTS%2BPerfectly+normal%2B%7EFirst+Countable
Observation: when I put "?" instead of "~" then a weird answer appears:
https://topology.pi-base.org/spaces?q=LOTS%2BPerfectly+normal%2B%3FFirst+Countable

Proof

Elementary:

By perfect normality, for $x\in X$ we have $\{x\}=\bigcap_{n=1}^\infty U_n$ for some descending sequence of open sets $U_n$. By definition of the order topology, we can replace $U_n$ by an open interval $(a_n,b_n)\subset U_n$, where $-\infty\leq a_n\leq a_{n+1}<x<b_{n+1}\leq b_n\leq +\infty$ (we introduce $\pm\infty$ to cover neighborhoods of minimal/maximal element in $X$).
For any $(a,b)\ni x$ there has to exist $m,n$ such that $a\leq a_n < x < b_m \leq b$. Otherwise either $[a,x]$ or $[x,b]$ would be contained in the intersection of $U_n$'s. Then $x\in(a_{n'},b_{n'})\subset(a,b)$ for $n'=\max(m,n)$. Hence we proven that $\{(a_n,b_n)\colon n\geq 1\}$ is a countable base of neighborhoods at $x$.

[Moniker1998]

This theorem doesn't need to exist. Try updating your version of pi-base

[Moniker1998]

The observation with the second link in your post is curious however. Any ideas why this search works like this @StevenClontz ?

[pzjp]

I was not aware that I can accidentally access old versions of the base.

[GeoffreySangston]

@pzjp On the pi-base website, you can click the circle of arrows at the bottom of your screen to reset pi-base (I believe without changing the branch). Or you can go to https://topology.pi-base.org/dev and click Reset, which will reset pi-base and set the branch to main.

[pzjp]

I've did this when the possibility of having outdated base was pointed out ;) I used to think that the date of migration refers to a global update I'm not able to interfere with.

[StevenClontz]

Reopened pi-base/web#166 to find a way to automatically resync when data is over a day old.

[StevenClontz]

The observation with the second link in your post is curious however. Any ideas why this search works like this @StevenClontz ?

It's buggy lol. 🤷‍♂️ I'm expecting to sync up with @jamesdabbs in the coming weeks to tackle a few things that he's more knowledgable about; I'll open an issue for this.

[StevenClontz]

Thanks for the contribution @pzjp - I'm closing as this seems to be deducable with an updated database.

[prabau]

@pzjp FYI, for a probable explanation of the "buggy behavior":

pi-base/web#205 (comment)