Upgrades T847 to 'locally euclidean => locally contractible'

Author: GeoffreySangston

theorems/T000847.md

@@ -3,12 +3,9 @@ uid: T000847
 if:
   P000122: true
 then:
-  P000230: true
-refs:
-  - zb: "0951.54001"
-    name: Topology (Munkres)
+  P000223: true
 ---
 
-A locally Euclidean space admits a basis of Euclidean open balls.
-For a Euclidean open ball $U$ and $x \in U$, $\pi_1(U,x)$ is trivial (see Example 1 on page 331 of {{zb:0951.54001}}).
-A Euclidean open ball is also path-connected. 
+A locally Euclidean space admits a basis of Euclidean open balls. A Euclidean open ball is homeomorphic to
+$\mathbb{R}^n$. Then the claim follows because the map $\mathbb{R}^n \times [0, 1] \to \mathbb{R}^n$,
+$(p, t) \mapsto (1-t)p$, is a homotopy from the identity map of Euclidean space to a constant map.