Real TVS Initial PR (#1746)

Author: GeoffreySangston

properties/P000087.md

@@ -8,7 +8,9 @@ refs:
     name: Topology (Munkres)
 ---
 
-There exists a continuous group operation $(x,y)\mapsto x\cdot y$ on the space such that
+$X$ is homeomorphic to a [topological group](https://en.wikipedia.org/wiki/Topological_group).
+
+Equivalently, there exists a continuous group operation $(x,y)\mapsto x\cdot y$ on $X$ such that
 the inverse operation $x\mapsto x^{-1}$ is also continuous.
 
 Contrary to Munkres or Willard, we do not assume any separation axiom like {P3}, {P2} or {P1}.

properties/P000238.md

@@ -0,0 +1,24 @@
+---
+uid: P000238
+name: Has a real TVS topology
+aliases:
+  - Topological vector space
+  - TVS
+refs:
+  - wikipedia: Topological_vector_space
+    name: Topological vector space on Wikipedia
+  - zb: "0867.46001"
+    name: Functional analysis (W. Rudin, 1991)
+---
+
+$X$ is homeomorphic to a [topological vector space](https://en.wikipedia.org/wiki/Topological_vector_space) (TVS) over $\mathbb R$.
+
+Equivalently, there exists a continuous commutative group operation $(x, y) \mapsto x + y$ on $X$, and a continuous scalar multiplication operation $\mathbb{R} \times X \to X$, $(\lambda, x) \mapsto \lambda x$, where $\mathbb{R}$ has the Euclidean topology, such that these operations together satisfy the axioms of a real vector space.
+
+Some others require separation axioms like {P3} or {P2}, though we do not.
+
+----
+#### Meta-properties
+
+- This property is preserved by arbitrary products.
+- This property is preserved by $\Sigma$-products.

spaces/S000103/properties/P000089.md

@@ -4,7 +4,7 @@ property: P000089
 value: true
 refs:
 - zb: "0867.46001"
-  name: Functional analysis. 2nd ed. (W. Rudin, 1991)
+  name: Functional analysis (W. Rudin, 1991)
 ---
 
 $X$ is a compact convex subset of a locally convex topological vector space $\mathbb R^I$. Therefore Schauder-Tychonoff fixed point theorem (Theorem 5.28 in {{zb:0867.46001}}) applies.

theorems/T000877.md

@@ -0,0 +1,11 @@
+---
+uid: T000877
+if:
+  and:
+  - P000238: true
+  - P000125: true
+then:
+  P000058: false
+---
+
+A nonzero real vector space contains a $1$-dimensional subspace, which is isomorphic to $\mathbb{R}$.

theorems/T000878.md

@@ -0,0 +1,9 @@
+---
+uid: T000878
+if:
+  P000238: true
+then:
+  P000087: true
+---
+
+By definition.

theorems/T000879.md

@@ -0,0 +1,9 @@
+---
+uid: T000879
+if:
+  P000238: true
+then:
+  P000199: true
+---
+
+A straight-line homotopy deformation retracts $X$ to the origin. That is, the map $X \times [0, 1] \to X$, $(x, t) \mapsto (1-t)x$ is a null-homotopy of the identity map.

theorems/T000880.md

@@ -0,0 +1,17 @@
+---
+uid: T000880
+if:
+  P000238: true
+then:
+  P000223: true
+refs:
+  - wikipedia: Balanced_set
+    name: Balanced set on Wikipedia
+  - zb: "0867.46001"
+    name: Functional analysis. 2nd ed. (W. Rudin)
+---
+
+Every neighborhood of the origin in a topological vector space $X$
+contains a balanced open neighborhood of the origin. See {{wikipedia:Balanced_set}}
+or Theorem 1.14(a) of {{zb:0867.4600}}.
+And a balanced set is {P199}.