Initial PR for Direct limit of finite-dimensional Euclidean spaces

spaces/S000106/README.md

@@ -0,0 +1,41 @@
+---
+uid: S000106
+name: Direct limit $\mathbb R^\infty$ of Euclidean spaces $\mathbb R^n$
+refs:
+  - wikipedia: Direct_limit
+    name: Direct limit on Wikipedia
+  - mathse: 3961052
+    name: Answer to "Is the weak topology on $\mathbb{R}^{\infty}$ the same as the box topology?"
+  - mathse: 5012784
+    name: Answer to "Is $\ell^\infty$ with box topology connected?"
+  - zb: "0298.57008"
+    name: Characteristic classes (Milnor-Stasheff)
+  - zb: "0307.55015"
+    name: Fibre bundles. 2nd ed. (Husemoller)
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+  - wikipedia: Fréchet–Urysohn_space
+    name: Fréchet–Urysohn space on Wikipedia
+---
+$X$ is the subset $\mathbb{R}^\infty$ of eventually $0$ sequences in $\mathbb{R}^\omega$,
+with the [final topology](https://en.wikipedia.org/wiki/Final_topology)
+with respect to the standard inclusion maps $\mathbb{R}^n \hookrightarrow \mathbb{R}^\infty$,
+$x \mapsto (x^1, \ldots, x^n, 0, \ldots)$.
+Thus, a set $U \subseteq \mathbb{R}^\infty$ is open iff $U \cap \mathbb{R}^n$
+is open in $\mathbb{R}^n$ for each $n$,
+where we identify each Euclidean space $\mathbb{R}^n$ with its image. 
+
+The space $\mathbb{R}^\infty$ is the [direct limit](https://en.wikipedia.org/wiki/Direct_limit)
+$\varinjlim \mathbb{R}^n$ of the direct system consisting of Euclidean spaces $\mathbb R^n$
+and standard inclusion maps $\mathbb{R}^n \hookrightarrow \mathbb{R}^m$,
+$x \mapsto (x^1, \ldots, x^n, 0, \ldots,0)$, for each $n < m$.
+
+Equivalently, $\mathbb{R}^\infty \subset \mathbb{R}^\omega$ has the subspace topology, where
+$\mathbb{R}^\omega$ is given the box topology; this is shown in {{mathse:3961052}}. Moreover,
+it is shown in {{mathse:5012784}} that $\mathbb{R}^\infty$ is a quasi-component of the origin in
+$\mathbb{R}^\omega$. Hence $\mathbb{R}^\infty$ embeds into {S107}
+as a path component.
+
+Defined on page 62 of {{zb:0298.57008}}, on page 2 of {{zb:0307.55015}}, 
+on page 56 of {{zb:1280.54001}}, and on {{wikipedia:Fréchet–Urysohn_space}} 
+under Direct limit of finite-dimensional Euclidean spaces.

spaces/S000106/properties/P000238.md

@@ -0,0 +1,16 @@
+---
+space: S000106
+property: P000238
+value: true
+refs:
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+---
+
+$\mathbb{R}^\infty$ with the natural scalar multiplication and addition operations is a vector space
+over $\mathbb{R}$. It remains to argue each operation is continuous.
+
+For each $n$, the scalar multiplication function $\mathbb{R} \times \mathbb{R}^\infty \to \mathbb{R}^\infty$ restricted to $\mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^n \hookrightarrow \mathbb{R}^\infty$ is continuous, since the first map identifies with the usual scalar multiplication of $n$-dimensional Euclidean space. Since {S25|P130}, Proposition 2.8.3 of {{zb:1280.54001}} implies $\mathbb{R} \times \mathbb{R}^\infty \cong \varinjlim (\mathbb{R} \times \mathbb{R}^n)$. This means that $\mathbb{R} \times \mathbb{R}^\infty$ has the final topology with respect to the inclusions 
+$\mathbb{R} \times \mathbb{R}^n \hookrightarrow \mathbb{R} \times \mathbb{R}^\infty$. By the universal property of the final topology, it follows that $\mathbb{R} \times \mathbb{R}^\infty \to \mathbb{R}^\infty$ is continuous.
+
+Since each $\mathbb{R}^n$ is locally compact, Proposition 2.8.4 of {{zb:1280.54001}} implies $\mathbb{R}^\infty \times \mathbb{R}^\infty \cong \varinjlim (\mathbb{R}^n \times \mathbb{R}^n)$. Making a similar argument as above shows that the natural addition operation on $\mathbb{R}^\infty$ is continuous. 

spaces/S000106/properties/P000240.md

@@ -0,0 +1,11 @@
+---
+space: S000106
+property: P000240
+value: true
+refs:
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+---
+
+The chain of subspaces $\empty \subset \mathbb{R}^0 \subset \mathbb{R}^1 \cdots$ is a CW structure.
+

spaces/S000107/README.md

@@ -1,6 +1,6 @@
 ---
 uid: S000107
-name: Countable box product of reals
+name: Countable box product of reals $\square^\omega\mathbb R$
 aliases:
   - Countable boolean product of reals
   - Box product topology on R^ω