TVS, two results about injectively path connected

theorems/T000925.md

@@ -0,0 +1,9 @@
+---
+uid: T000925
+if:
+  P000238: true
+then:
+  P000038: true
+---
+
+If $x, y\in X, x\neq y$, then $p(t) = (1-t)x+ty$ for $t\in [0, 1]$ is an injective path from $x$ to $y$.

theorems/T000926.md

@@ -0,0 +1,16 @@
+---
+uid: T000926
+if:
+  P000238: true
+then:
+  P000043: true
+refs:
+  - zb: "0867.46001"
+    name: Functional analysis (W. Rudin, 1991)
+---
+
+Since any TVS is {P86} [(Explore)](https://topology.pi-base.org/spaces?q=TVS+%2B+not+homogeneous), it is enough to find a local base of injectively path connected open neighborhoods for the origin $0$.
+Note that $X$ has a neighbourhood base for $0$ consisting of [balanced](https://en.wikipedia.org/wiki/Balanced_set) open sets (see Theorem 1.14(a) in {{zb:0867.46001}}),
+and any such set $U$ is injectively path connected:
+if the distinct points $y_1, y_2\in U$ are collinear with 0, take a linear path from $y_1$ to $y_2$;
+otherwise, take a linear path from $y_1$ to $0$ followed by one from $0$ to $y_2$.