New P97: Embeddable in the real line

[prabau]

Add new property P97: Embeddable in $\mathbb R$

New theorems to accompany this:

• (T231) embeddable in R ==> embeddable in Euclidean space
• (T232) totally path disconnected + embeddable in R ==> zero dimensional
• (T233) connected + embeddable in R ==> locally path connected
• (updated T462) separable + metrizable + zero dimensional ==> embeddable in R
• (updated T463) LOTS + second countable ==> embeddable in R

These theorems allow to determine whether P97 holds or not for many spaces. For all the remaining spaces known as "embeddable in Euclidean space" with P97 undetermined, added some explicit trait files as needed.

And more updates for S121 (Bernstein's connected set), S147 (Luzin set), S148 (Luzin set).

[ccaruvana]

Taking a look here and I have a quick question. This PR asserts P65 for S121, which is automatically deduced currently. I would assume that the change in asserted properties for S121 in this PR makes the automatic deduction of P65 impossible. Without taking an in depth look at the deduction tree (https://topology.pi-base.org/spaces/S000121/properties/P000065), is there another way to check why P65 isn't deduced for S121 with the content of this PR?

[ccaruvana]

Maybe this was mentioned in our last community call, but I've gotten a couple of 404s using "open link in new tab" for theorems and asserted properties in this PR while browsing. When I don't use the "open link in new tab" and just click directly, they seem to work fine and I can see no difference in the displayed URLs.

[StevenClontz]

So the 404 is triggering based upon the pages that exist in the main branch, when visited directly. As pointed out this is only when a page is loaded from scratch - internal routing works fine.

This is a wontfix for now as it only affects reviewers of non-main branches, as annoying as it is.

[ccaruvana]

I've checked over everything except for T463 in detail since it references a new mathse post which is involved. If no one else beats me to it, I'll think it about in more detail a bit later.

In the meantime, I believe what's written for T233, but would anyone think it beneficial to throw in some basic reference?

[prabau]

Taking a look here and I have a quick question. This PR asserts P65 for S121, which is automatically deduced currently. I would assume that the change in asserted properties for S121 in this PR makes the automatic deduction of P65 impossible. Without taking an in depth look at the deduction tree (https://topology.pi-base.org/spaces/S000121/properties/P000065), is there another way to check why P65 isn't deduced for S121 with the content of this PR?

The previous justification for S121/P65 (https://topology.pi-base.org/spaces/S000121/properties/P000065) seemed extremely long, and depended on the asserted P129 (indiscrete) = false. It seems simpler to assert P65 directly, as it's pretty immediate from the construction of the space, and make P129 deduced instead.

(Many spaces assert P129 directly, and don't need to. I think it's a holdover of some old PR where the property was asserted for nearly all spaces.)

[prabau]

I believe what's written for T233, but would anyone think it beneficial to throw in some basic reference?

Not sure what to add, but feel free to modify T233 as you see fit.

[prabau]

Another general question (not specific to this PR, but affects it also). In the browser the reference names are not expanded for latex/mathjax. See for example "mathbb R" in https://topology.pi-base.org/spaces/S000140/references.

Do you think it could be expanded at some point in the future?

[StevenClontz]

Another general question (not specific to this PR, but affects it also). In the browser the reference names are not expanded for latex/mathjax. See for example "mathbb R" in https://topology.pi-base.org/spaces/S000140/references.

Do you think it could be expanded at some point in the future?

The issue is that when you write {{mr:123456}}, the component that renders it to a link is unaware of any reference data provided elsewhere in that text file or otherwise.

I'd prefer some kind of solution that allows us to only provide ids, and then some external API provides the title, e.g. https://api.zbmath.org/v1/

[prabau]

The issue is that when you write {{mr:123456}}, the component that renders it to a link is unaware of any reference data provided elsewhere in that text file or otherwise.

I was not talking about the expansion of something like {{mr:123456}}, but instead about the list of references in a "References" page. The contents of that list is constructed from the name: fields in the refs: section from the metadata.

[StevenClontz]

The issue is that when you write {{mr:123456}}, the component that renders it to a link is unaware of any reference data provided elsewhere in that text file or otherwise.

I was not talking about the expansion of something like {{mr:123456}}, but instead about the list of references in a "References" page. The contents of that list is constructed from the name: fields in the refs: section from the metadata.

Oh gotcha. Open an issue in /web and assign me and I can maybe take a crack at this.

[prabau]

Hmm, thanks for approving. But I think it would have been better to let Chris do it, as he was planning to do it. Also, when there is still work going on, seems better for that to be complete first.

[StevenClontz]

Assigning to @ccaruvana

[ccaruvana]

Haha I didn't mean to claim ownership over approving, but thanks for keeping me in on the loop. Based on the conversation, this PR seems ready to go and the GO space will be added later (go GO).

[Jianing-Song]

As for a converse of LOTS + second countable ==> embeddable in $\mathbb{R}$, we need a space embeddable in $\mathbb{R}$ that is not a LOTS.

I propose the space $X$ that is the disjoint union of $\mathbb{R}$ and an extra point $\infty$. It is clearly embeddable in $\mathbb{R}$ as $(0,1)\cup\{2\}$. To show that it is not a LOTS, note that in the opposite situation $\infty$ must be either the largest or the smallest element of $X$, otherwise $(\leftarrow,\infty)$ and $(\infty,\rightarrow)$ is an open partition of $X\setminus\{\infty\}$ which is connected, impossible.

Suppose WLOG that $\infty$ is the largest element, then ${\infty}$ is open implies that $\mathbb{R}$ contains a largest element. But then removing the largest element from $\mathbb{R}$ results in a space that is still connected in the subspace topology of $X$ (*), and removing any point from $\mathbb{R}$ results in a disconnected space in the usual topology.

(*) Removing the largest element $a$ of a LOTS leaves a space whose subspace topology coincides with the order topology. The remaining space is connected if the original space is: For LOTS connectedness $\Leftrightarrow$ complete dense order, and we can see that the completeness (the existence of all infima) is preserved. Also, completeness is equivalent to every bounded closed interval is compact, which is clearly preserved. For more information about completeness of LOTS, see https://en.wikipedia.org/wiki/Completeness_(order_theory).

[prabau]

@Jianing-Song Good example to have, with great justification here.

One minor thing. It's true that for a connected LOTS with a maximum element, removing that maximum still gives a connected space. But connected LOTS is not exactly that same as order-dense + order-complete. Order-complete means every subset has a supremum. But we need instead: every subset with an upper bound has a least upper bound. It's what the wikipedia article calls "bounded complete" (not sure how common that terminology is though).

[Jianing-Song]

@Jianing-Song Good example to have, with great justification here.

One minor thing. It's true that for a connected LOTS with a maximum element, removing that maximum still gives a connected space. But connected LOTS is not exactly that same as order-dense + order-complete. Order-complete means every subset has a supremum. But we need instead: every subset with an upper bound has a least upper bound. It's what the wikipedia article calls "bounded complete" (not sure how common that terminology is though).

OK, but then being order-complete is just the same thing as being compact. Strange enough!

[prabau]

Yes, order-complete is the same as being compact.

[prabau]

I missed one detail. The "bounded complete" property, more commonly called "least upper bound property" it seems, should be: Every nonempty subset with an upper bound has a least upper bound.

(Seems wikipedia is missing this nonempty qualifications in a few places)