Locally Simply Connected Initial PR

properties/P000230.md

@@ -0,0 +1,19 @@
+---
+uid: P000230
+name: Locally simply connected
+refs:
+  - wikipedia: Locally simply connected space
+    name: Locally simply connected space on Wikipedia
+  - mr: 2766102
+    name: Introduction to topological manifolds (Lee)
+  - zb: "0951.54001"
+    name: Topology (Munkres)
+  - mo: 487326
+    name: 'Definition of locally simply connected space'
+---
+
+$X$ admits a basis of open sets which are {P200}.
+
+Equivalently, for every $x \in X$ and each neighborhood $N$ of $x$ in $X$, there is a simply connected open neighborhood $U$ of $x$ contained in $N$.
+
+Defined on page 298 of {{mr:2766102}}, page 495 of {{zb:0951.54001}} and as property $P_1$ of {{mo:487326}}.

properties/P000231.md

@@ -0,0 +1,13 @@
+---
+uid: P000231
+name: Weakly locally simply connected
+refs:
+  - zb: "0063.00842"
+    name: Theory of Lie groups. I (Chevalley)
+  - mo: 487326
+    name: 'Definition of locally simply connected space'
+---
+
+Every point of $X$ has a neighborhood which is {P200}. 
+
+Defined as "locally simply connected" on page 54 of {{zb:0063.00842}} and as property $P_4$ of {{mo:487326}}.

properties/P000232.md

@@ -0,0 +1,25 @@
+---
+uid: P000232
+name: $LC^1$
+aliases:
+  - Locally simply connected
+refs:
+  - zb: "0153.52905"
+    name: Theory of retracts (Borsuk)
+  - mo: 487326
+    name: 'Definition of locally simply connected space'
+  - mathse: 5126526
+    name: Is Borsuk's definition of $LC^1$ equivalent to this formulation of 'locally simply connected' ($P_{10}$)?
+---
+
+$X$ is locally $0$-connected and locally $1$-connected, as in {{zb:0153.52905}}.
+A space $X$ is locally $n$-connected if for every $x \in X$ and each neighborhood $N$ of $x$ in $X$, there is a neighborhood $U$ of $x$ contained in $N$ such that every map $S^n \to N$ with values in $U$ is null-homotopic in $N$.
+
+Equivalently, for every $x \in X$ and each neighborhood $N$ of $x$ in $X$, there is a path-connected neighborhood $U$ of $x$ contained in $N$ such that every loop in $U$ is null-homotopic in $N$. See {{mathse:5126526}}.
+
+This property is part of a hierarchy of $LC^n$ properties which includes {P42} as $LC^0$.
+Defined on page 54 of {{zb:0153.52905}} and as property $P_{10}$ of {{mo:487326}}.
+
+----
+#### Meta-properties
+- This property is preserved by retractions.

theorems/T000847.md

@@ -3,11 +3,11 @@ uid: T000847
 if:
   P000122: true
 then:
-  P000229: true
+  P000230: true
 refs:
   - zb: "0951.54001"
     name: Topology (Munkres)
 ---
 
-For $x \in X$ pick a neighborhood $U$ homeomorphic to $\mathbb{R}^n$.
-Then $\pi_1(U,x)$ is trivial (see Example 1 on page 331 of {{zb:0951.54001}}).
+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}}).

theorems/T000848.md

@@ -3,7 +3,7 @@ uid: T000848
 if:
   P000090: true
 then:
-  P000229: true
+  P000230: true
 refs:
 - mathse: 2965374
   name: Answer to "Are minimal neighborhoods in an Alexandrov topology path-connected?"

theorems/T000853.md

@@ -0,0 +1,9 @@
+---
+uid: T000853
+if:
+  P000230: true
+then:
+  P000231: true
+---
+
+Immediate from the definitions.

theorems/T000854.md

@@ -0,0 +1,9 @@
+---
+uid: T000854
+if:
+  P000230: true
+then:
+  P000232: true
+---
+
+Immediate from the equivalent characterizations of each property.

theorems/T000855.md

@@ -0,0 +1,9 @@
+---
+uid: T000855
+if:
+  P000231: true
+then:
+  P000229: true
+---
+
+Immediate from the definitions.

theorems/T000856.md

@@ -0,0 +1,17 @@
+---
+uid: T000856
+if:
+  P000232: true
+then:
+  P000229: true
+refs:
+- mathse: 4044399
+  name: Characterizing simply connected spaces
+---
+
+Let $x \in X$. By {P232}, there exists a path-connected neighborhood $U$ of $x$ such that every 
+loop $ S^1 \to X$ loop with image in $U$ is null-homotopic. Let $\sigma$ be a loop in $U$ based at $x$. 
+Choose a null-homotopy $F : S^1 \times [0, 1] \to X$ from $\sigma$ to a constant loop. Apply the arguments 
+$(4) \Rightarrow (5)$ and $(5) \Rightarrow (1)$ from {{mathse:4044399}} to $F$ in order to construct a 
+basepoint preserving null-homotopy of $\sigma$ to the constant loop at $x$. 
+Then {P229} follows.

theorems/T000857.md

@@ -0,0 +1,9 @@
+---
+uid: T000857
+if:
+  P000232: true
+then:
+  P000042: true
+---
+
+$LC^1$ implies $LC^0$ by definition.