diff --git a/properties/P000230.md b/properties/P000230.md
new file mode 100644
index 000000000..c33916d4d
--- /dev/null
+++ b/properties/P000230.md
@@ -0,0 +1,17 @@
+---
+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: "1030.57035"
+    name: Bing's dogbone space is not strongly locally simply connected
+---
+
+$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}}, page 495 of {{zb:0951.54001}} and as property $P_1$ of {{mo:487326}}. Has also been called "strongly locally simply connected", for example in {{zb:1030.57035}}.
diff --git a/properties/P000231.md b/properties/P000231.md
new file mode 100644
index 000000000..2c7f69a5f
--- /dev/null
+++ b/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}}.
diff --git a/properties/P000232.md b/properties/P000232.md
new file mode 100644
index 000000000..d3a48dd89
--- /dev/null
+++ b/properties/P000232.md
@@ -0,0 +1,27 @@
+---
+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}$)?
+  - zb: "0198.56303"
+    name: Acyclicity in three-manifolds
+---
+
+$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 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}}.
+
+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}}. Has also been called "locally simply connected", for example in {{zb:0198.56303}}.
+
+----
+#### Meta-properties
+- This property is preserved by retractions.
diff --git a/theorems/T000847.md b/theorems/T000847.md
index 1c68ff60f..131e5ba0e 100644
--- a/theorems/T000847.md
+++ b/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}}).
+The claim follows because $\mathbb{R}^n$ is contractible, and {T583}.
diff --git a/theorems/T000848.md b/theorems/T000848.md
index 93c4720bb..3ef87964f 100644
--- a/theorems/T000848.md
+++ b/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?"
diff --git a/theorems/T000853.md b/theorems/T000853.md
new file mode 100644
index 000000000..e6b957eec
--- /dev/null
+++ b/theorems/T000853.md
@@ -0,0 +1,9 @@
+---
+uid: T000853
+if:
+  P000230: true
+then:
+  P000231: true
+---
+
+Immediate from the definitions.
diff --git a/theorems/T000854.md b/theorems/T000854.md
new file mode 100644
index 000000000..f7b145bcf
--- /dev/null
+++ b/theorems/T000854.md
@@ -0,0 +1,9 @@
+---
+uid: T000854
+if:
+  P000230: true
+then:
+  P000232: true
+---
+
+Immediate from the equivalent characterizations of each property.
diff --git a/theorems/T000855.md b/theorems/T000855.md
new file mode 100644
index 000000000..8dbd02379
--- /dev/null
+++ b/theorems/T000855.md
@@ -0,0 +1,9 @@
+---
+uid: T000855
+if:
+  P000231: true
+then:
+  P000229: true
+---
+
+Immediate from the definitions.
diff --git a/theorems/T000856.md b/theorems/T000856.md
new file mode 100644
index 000000000..d681b476c
--- /dev/null
+++ b/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.
diff --git a/theorems/T000857.md b/theorems/T000857.md
new file mode 100644
index 000000000..a3df3fa5c
--- /dev/null
+++ b/theorems/T000857.md
@@ -0,0 +1,9 @@
+---
+uid: T000857
+if:
+  P000232: true
+then:
+  P000042: true
+---
+
+$LC^1$ implies $LC^0$ by definition.