Locally Simply Connected Initial PR

properties/P000229.md

@@ -14,7 +14,7 @@ refs:
 
 Every point $x \in X$ has a neighborhood $U$ such that the homomorphism $i_*:\pi_1(U, x) \to\pi_1(X,x)$ of fundamental groups induced by the inclusion $i: U \hookrightarrow X$ is trivial.
 
-Equivalently, for every loop based at $x$ whose image lies in $U$, there exists a basepoint-preserving homotopy in $X$ to the constant loop at $x$.
+Equivalently, every point $x \in X$ has a neighborhood $U$ such that for every loop in $U$ based at $x$ there exists a basepoint-preserving homotopy in $X$ to the constant loop at $x$.
 
 Defined on page 494 of {{zb:0951.54001}} and on page 63 of {{zb:1044.55001}}.
 

properties/P000230.md

@@ -0,0 +1,19 @@
+---
+uid: P000230
+name: Locally simply connected
+refs:
+  - zb: "1209.57001"
+    name: Introduction to topological manifolds (Lee)
+  - mo: 487326
+    name: 'Definition of locally simply connected space'
+  - zb: "0209.54802"
+    name: On the strong local simple connectivity of the decomposition spaces of toroidal decompositions (S. Armentrout)
+---
+
+$X$ admits a basis of open sets which are {P200}.
+
+Equivalently, for each $x \in X$, every neighborhood of $x$ contains a simply connected open neighborhood of $x$.
+
+Defined on page 298 of {{zb:1209.57001}}, and listed as property $P_1$ in {{mo:487326}}.
+
+Has also been called "strongly locally simply connected", for example in {{zb:0209.54802}}.

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 listed as property $P_4$ in {{mo:487326}}.

properties/P000232.md

@@ -0,0 +1,39 @@
+---
+uid: P000232
+name: $LC^1$
+aliases:
+  - Locally simply connected
+  - Locally $1$-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}$)?
+  - zb: "0198.56303"
+    name: Acyclicity in three-manifolds (McMillan)
+  - zb: "0234.55001"
+    name: Lectures on algebraic topology (Dold)
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+---
+
+$X$ is *locally $0$-connected* and *locally $1$-connected*.
+
+Following Borsuk's terminology (see page 30 of {{zb:0153.52905}}), this is the case $n=1$ in the hierarchy of $LC^n$ properties.
+A space $X$ is *locally $n$-connected* if for each $x\in X$ every neighborhood $N$ of $x$ contains a neighborhood $U$ of $x$
+such that every map $S^n \to N$ with values in $U$ is null-homotopic in $N$.
+And $X$ satisfies the $LC^n$ property if it is locally $k$-connected for $k=0,1,\dots,n$.
+(Note: $LC^0$ is equivalent to {P42}.)
+
+Equivalently, for each $x \in X$, every neighborhood $N$ of $x$ contains a {P37} neighborhood $U$ of $x$
+such that every loop $\phi:S^1\to U$ is null-homotopic in $N$. See {{mathse:5126526}}.
+
+Some authors, for example {{zb:0234.55001}} and {{zb:1280.54001}}, use "locally 1-connected" with the meaning of $LC^1$.
+Has also been called "locally simply connected", for example in {{zb:0198.56303}}.
+Listed as property $P_{10}$ in {{mo:487326}}.
+
+----
+#### Meta-properties
+- This property is preserved by retractions (use Theorem 16.2 on p. 29 of {{zb:0153.52905}}).

theorems/T000847.md

@@ -3,11 +3,12 @@ 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}}).
+A Euclidean open ball is also path-connected. 

theorems/T000848.md

@@ -3,10 +3,10 @@ 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?"
 ---
 
-For each point $x \in X$, the minimal neighborhood $U_x$ of $x$ is {P199} (see {{mathse:2965374}}) and thus {P200} by {T583}.
+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}.

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$. From {P232} it follows that there is a path-connected neighborhood $U$ of $x$ such that every
+loop $S^1 \to X$ loop with image in $U$ is null-homotopic in $X$. In particular, 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.

theorems/T000858.md

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