Locally contractible initial PR (#1722)

Author: GeoffreySangston

properties/P000223.md

@@ -0,0 +1,13 @@
+---
+uid: P000223
+name: Locally contractible
+refs:
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+$X$ admits a basis of open sets which are {P199}.
+
+Equivalently, for each $x \in X$, every neighborhood of $x$ contains a {P199} open neighborhood of $x$.
+
+"Locally contractible" is used in {{zb:1044.55001}}, where it is defined informally with the meaning above as part of the statement of Proposition A.4 on page 522.  (As explained on page 61, the book follows the convention of a space being "locally P" for a property P to mean that every point has arbitrarily small open neighborhoods with the property; this is very close to the [general convention used in pi-base](https://github.com/pi-base/data/wiki/Conventions-and-Style#Local-Properties).)

properties/P000224.md

@@ -0,0 +1,17 @@
+---
+uid: P000224
+name: Weakly locally contractible
+refs:
+  - zb: "0087.38203"
+    name: On fiber spaces (Fadell)
+  - zb: "0642.54014"
+    name: LECS, local mixers, topological groups and special products (Borges)
+---
+
+Every point of $X$ has a neighborhood which is {P199}. 
+
+The name we have chosen for this property conforms to the [pi-base naming conventions](https://github.com/pi-base/data/wiki/Conventions-and-Style#Local-Properties).
+However, we have not seen this property mentioned with a specific name in the literature.
+
+The terminology "weakly locally contractible" has been used for multiple concepts different from this one, but the name is not standardized.
+A relatively common usage among those is as a synonym for "semilocally contractible" (see {{zb:0087.38203}} and {{zb:0642.54014}}).

properties/P000225.md

@@ -0,0 +1,26 @@
+---
+uid: P000225
+name: $LC$
+aliases:
+  - Locally contractible
+refs:
+  - zb: "0153.52905"
+    name: Theory of retracts (Borsuk)
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+  - zb: "1059.54001"
+    name: Encyclopedia of general topology
+---
+
+$X$ is *locally contractible at the point* $x$ for all $x \in X$,
+in the sense that every neighborhood $U$ of $x$ contains a neighborhood (equivalently, an open neighborhood) $V$ of $x$ that is contractible in $U$;
+i.e., such that the inclusion map $V \hookrightarrow U$ is null-homotopic.
+
+Equivalently, every neighborhood $U$ of any point $x$ contains a neighborhood (or an open neighborhood) $V$ of $x$
+such that the inclusion map $V \hookrightarrow U$ is homotopic to the constant map with value $x$.
+
+This is the standard definition of "locally contractible" in the theory of ANRs, as originally introduced by Borsuk. Defined as *locally contractible* on page 28 of {{zb:0153.52905}}, page 347 of {{zb:1280.54001}}, and page 341 of {{zb:1059.54001}}. The abbreviation $LC$ is commonly used in this context.
+
+----
+#### Meta-properties
+- This property is preserved by retractions (Theorem 15.3 on p. 28 of {{zb:0153.52905}}).

theorems/T000847.md

@@ -3,12 +3,8 @@ 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. 
+For each $x\in X$, every neighborhood of $x$ contains an open neighborhood homeomorphic to some Euclidean space $\mathbb R^n$.
+And $\mathbb R^n$ is {P199} as it can be deformation retracted to a point using a straight-line homotopy.

theorems/T000848.md

@@ -3,10 +3,10 @@ uid: T000848
 if:
   P000090: true
 then:
-  P000230: true
+  P000223: true
 refs:
 - mathse: 2965374
   name: Answer to "Are minimal neighborhoods in an Alexandrov topology path-connected?"
 ---
 
-For each point $x \in X$, the minimal neighborhood $U_x$ of $x$ is open and {P199} (see {{mathse:2965374}}). By {T583}, $U_x$ is {P200}.
+For each point $x \in X$, the minimal neighborhood $U_x$ of $x$ is open and {P199} (see {{mathse:2965374}}).

theorems/T000867.md

@@ -0,0 +1,9 @@
+---
+uid: T000867
+if:
+  P000223: true
+then:
+  P000224: true
+---
+
+Immediate from the definitions.

theorems/T000868.md

@@ -0,0 +1,9 @@
+---
+uid: T000868
+if:
+  P000223: true
+then:
+  P000225: true
+---
+
+Immediate from the definitions.

theorems/T000869.md

@@ -0,0 +1,9 @@
+---
+uid: T000869
+if:
+  P000223: true
+then:
+  P000230: true
+---
+
+By {T583}.

theorems/T000870.md

@@ -0,0 +1,9 @@
+---
+uid: T000870
+if:
+  P000224: true
+then:
+  P000231: true
+---
+
+By {T583}.

theorems/T000871.md

@@ -0,0 +1,10 @@
+---
+uid: T000871
+if:
+  P000225: true
+then:
+  P000232: true
+---
+
+If $V$ is contractible in $U$, any map $Y \to V$ is null-homotopic in $U$.
+Apply this to $Y=S^0, S^1$.