Initial commit of locally contractible properties

Author: GeoffreySangston

properties/P000223.md

@@ -0,0 +1,8 @@
+---
+uid: P000223
+name: Locally contractible
+---
+
+$X$ admits a basis of open sets which are {P199}.
+
+The naming of this property follows pi-base conventions.

properties/P000224.md

@@ -0,0 +1,13 @@
+---
+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 naming of this property follows pi-base conventions. The name "weakly locally contractible" is commonly used in literature instead as an alias for "semi-locally contractible"; see for instance {{zb:"0087.38203"}} and {{zb:"0642.54014"}}.

properties/P000225.md

@@ -0,0 +1,23 @@
+---
+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 $LC$ if every neighborhood $U$ of any point $x$ contains a neighborhood $V$ of $x$ that is contractible in $U$. 
+
+Equivalently, $X$ is locally contractible at each of its points. A space $X$ is *locally contractible at a point* $x \in X$ if every neighborhood $U$ of $x$ contains a neighborhood $V$ of $x$ such that the inclusion map $V \to U$ is null-homotopic.
+
+This is the standard definition of "locally contractible" in the theory of ANRs. Defined as "locally contractible" on page 28 of {{zb:0153.52905}}, page 347 of {{zb:"1280.54001"}}, and page 341 of {{zb:"1059.54001"}}.
+
+----
+#### Meta-properties
+- This property is preserved by retractions (Theorem 15.3 on p. 28 of {{zb:0153.52905}}).

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 by the definitions.

theorems/T000868.md

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

theorems/T000869.md

@@ -0,0 +1,9 @@
+---
+uid: T000869
+if:
+  P000223: true
+then:
+  P000230: true
+---
+
+A contractible space is simply connected.

theorems/T000870.md

@@ -0,0 +1,9 @@
+---
+uid: T000870
+if:
+  P000224: true
+then:
+  P000231: true
+---
+
+A contractible space is simply connected.

theorems/T000871.md

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