Box product of real lines is SLSC

[GeoffreySangston]

It can also be shown directly that $F$ is continuous (via $\epsilon$$\delta$ style argument). The version here is probably more useful though. This argument (and/or the direct argument that $F$ is continuous) might be better done in an MSE thread.

Edit: I'm not sure how to remove P234 from Files changed. I think I split this branch off of the branch used to commit that file. That file has not changed at all and already exists in main, so can be ignored.

[prabau]

Yeah, it seems a little much for a direct pi-base proof.

[prabau]

For removing the spurious P234 from Files changed, you can do "git rebase main" if you use a command line terminal.

[prabau]

I looked at it directly and it seems ok for a direct proof in pi-base.

[prabau]

It would be easier to use subscripts $y_n$, $x_m$ for the components of elements.
The superscripts are confusing (in his posts, Moniker used superscripts for different elements).

[prabau]

The first mathse link is missing from the refs:.

[prabau]

Regarding the "weak topology" thing, I know it's used in this context. Maybe it's old terminology? But I have always found it confusing, as it is the final topology wrt the inclusions $\mathbb R^n\to\mathbb R^\infty$, i.e., the strongest topology that makes the inclusions continuous.

[prabau]

deferring to @Moniker1998 for the meat of this

[prabau]

Side remark: I think $\mathbb R^\infty$ would be interesting to add as a separate space at some point in the future.

$\mathbb R^\infty\subseteq\mathbb R^\omega$ appears in Munkres problem 7 on p. 118.
Is that a common notation for that space? I vaguely remember it appears also as an example in functional analysis, but I am not sure.

[Moniker1998]

Side remark: I think R ∞ would be interesting to add as a separate space at some point in the future.

R ∞ ⊆ R ω appears in Munkres problem 7 on p. 118. Is that a common notation for that space? I vaguely remember it appears also as an example in functional analysis, but I am not sure.

@prabau I think this space is most common in algebraic topology, where it appears as a CW-complex

[Moniker1998]

deferring to @Moniker1998 for the meat of this

@prabau I had a different proof in mind for second part of semilocally simply connected, and I'm not into this whole colimit stuff, so feel free to check that yourself. The part about open components is of course correct.

Namely, you can show by an easy argument that if $K\subseteq \mathbb{R}^\infty$ is compact, then $K\subseteq \mathbb{R}^n$ for some $n$, and so when we talk about loops, we are talking about them in $\mathbb{R}^n$. (this was before I knew this space coincides with the CW-complex space)

Also, the math.se post that $\mathbb{R}^\infty$ is the connected path-component at $0$ is not cited in the references, not sure if this is intentional.

[GeoffreySangston]

I think we should add $$\mathbb{R}^\infty$$ and close this PR actually, since this trait will effectively just become a link to the trait saying that $$\mathbb{R}^\infty$$ is contractible (actually SLSC, derived from contractible); and this space (box product of real lines) will include in its description links indicating that $$\mathbb{R}^\infty$$ is a component (and or path component / quasi-component).

Visting family today and tomorrow but I'll get to this when I can.

[Moniker1998]

@GeoffreySangston alright, for now I'm putting it as a draft and you can decide later. Closing it might be a good idea.

[prabau]

The space $\mathbb R^\infty$ is described in some detail in
https://en.wikipedia.org/wiki/Fr%C3%A9chet%E2%80%93Urysohn_space#Examples
as "Direct limit of finite-dimensional Euclidean spaces".

[Moniker1998]

@prabau Interesting how $\mathbb{R}^\omega$ with box topology is not sequential, but $\mathbb{R}^\infty$ with box topology is sequential, but not Frechet-Urysohn.