T709: path connected + US => injectively path connected (#1260)

properties/P000095.md

@@ -11,7 +11,7 @@ refs:
 Given any two distinct points $x,y\in X$, there is an *arc* in $X$ from $x$ to $y$;
 that is, a homeomorphic embedding $f:[0,1]\to X$ with $f(0)=x$ and $f(1)=y$.
 
-See Definition 27.1 in {{zb:1052.54001}}, which uses the usual definition of "arc" from the literature.
+See Definition 27.1 in {{zb:1052.54001}}, which uses this usual definition of "arc" from the literature.
 
 Compare with {P37} and {P38}.
 

theorems/T000240.md

@@ -3,18 +3,26 @@ uid: T000240
 if:
   and:
   - P000037: true
-  - P000003: true
+  - P000143: true
 then:
   P000095: true
 refs:
 - mathse: 4247643
   name: Answer to "Does path-connected imply simple path-connected?"
 - zb: "1052.54001"
   name: General Topology (Willard)
+- mathse: 964546
+  name: Answer to "Weak Hausdorff space not KC"
 ---
 
-See Jeremy Brazas's
+It is a classical result that {P37} {P3} spaces are {P95}.
+This is shown for example in Jeremy Brazas's
 [expository note](https://www.wcupa.edu/sciences-mathematics/mathematics/jBrazas/documents/Constructing_arcs_from_paths_9-9-21.pdf)
 referenced from {{mathse:4247643}}.
-
 See also Corollary 31.6 in {{zb:1052.54001}}.
+
+Now suppose $X$ is {P37} and {P143}.
+Given two distinct points $x,y\in X$ and a path $f:[0,1]\to X$,
+the image $f([0,1])$ is Hausdorff (for example from Lemma 1 in {{mathse:964546}}).
+By the classical case above, there is an arc (homeomorphic embedding) from $x$ to $y$
+within $f([0,1])$, which is also an arc in $X$.

theorems/T000709.md

@@ -0,0 +1,14 @@
+---
+uid: T000709
+if:
+  and:
+  - P000037: true
+  - P000099: true
+then:
+  P000038: true
+refs:
+  - mathse: 4862260
+    name: Answer to "Does path-connected imply simple path-connected?"
+---
+
+See {{mathse:4862260}}.