diff --git a/properties/P000240.md b/properties/P000240.md
new file mode 100644
index 000000000..4dd91a8b0
--- /dev/null
+++ b/properties/P000240.md
@@ -0,0 +1,39 @@
+---
+uid: P000240
+name: CW complex
+refs:
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+  - zb: "0207.21704"
+    name: The Topology of CW Complexes (Lundell & Weingram)
+  - wikipedia: CW_complex
+    name: CW complex on Wikipedia
+---
+
+$X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subseteq \dots$, such that:
+
+- $X_n$ is obtained from $X_{n-1}$ by attaching $n$-cells.
+- $X = \bigcup_{n\geq 0} X_n$ and a subspace $U \subseteq X$ is open iff $U \cap X_n$ open in $X_n$ for all $n \geq -1$.
+
+Here *attaching $n$-cells* means that there is a discrete space $J$, and for every $j \in J$ a continuous map $f_j:\partial D^n \to X_{n-1}$, such that $X_n$ is homeomorphic to the quotient $(X_{n-1} \sqcup (J \times D^n)) /{\sim}$,
+where $\sim$ is the equivalence relation generated by $(j,x) \sim f_j(x)$ for all $(j,x)\in J \times \partial D^n$.
+The set $J$ is allowed to be empty, in which case $X_n=X_{n-1}$.
+The $0$-skeleton $X_0$ has the discrete topology; if it is empty, $X$ itself is empty.
+
+Here $D^n$ is the closed unit disk in $\mathbb R^n$ and $\partial D^n=S^{n-1}$ is the unit sphere in $\mathbb R^n$. We set $\partial D^0=S^{-1}=\emptyset$ by convention.
+
+*Note*: A *CW-structure* on a topological space $X$ is a filtration $X_{-1}\subseteq X_0\subseteq X_1 \subseteq\dots$ satisfying the conditions above.
+Strictly speaking, a *CW complex* is a space $X$ together with a compatible CW-structure.
+For simplicity and by a slight abuse of language, we call the space itself a CW complex if it admits a CW structure.
+
+Defined on page 5 of {{zb:1044.55001}}, also given in Theorem II.2.4 of {{zb:0207.21704}}.
+See also <https://ncatlab.org/nlab/show/CW+complex>.
+
+----
+An equivalent definition can be given in terms of a decomposition of $X$ into cells and conditions on their associated characteristic maps.
+For details and the meaning of this terminology, see Proposition A.2 on page 521 of {{zb:1044.55001}} or Definition II.1.1 in {{zb:0207.21704}}.
+
+----
+#### Meta-properties
+
+- This property is preserved by arbitrary disjoint unions.
diff --git a/theorems/T000883.md b/theorems/T000883.md
new file mode 100644
index 000000000..91d6f0c1f
--- /dev/null
+++ b/theorems/T000883.md
@@ -0,0 +1,12 @@
+---
+uid: T000883
+if:
+  P000240: true
+then:
+  P000067: true
+refs:
+  - zb: "0207.21704"
+    name: The Topology of CW Complexes (Lundell, Weingram)
+---
+
+See Proposition II.4.3 in {{zb:0207.21704}}, where "perfectly normal" is defined as {P67}.
diff --git a/theorems/T000884.md b/theorems/T000884.md
new file mode 100644
index 000000000..7ae33cddb
--- /dev/null
+++ b/theorems/T000884.md
@@ -0,0 +1,12 @@
+---
+uid: T000884
+if:
+  P000240: true
+then:
+  P000223: true
+refs:
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+See Proposition A.4 in {{zb:1044.55001}}.
diff --git a/theorems/T000885.md b/theorems/T000885.md
new file mode 100644
index 000000000..ea8a01b98
--- /dev/null
+++ b/theorems/T000885.md
@@ -0,0 +1,12 @@
+---
+uid: T000885
+if:
+  P000240: true
+then:
+  P000030: true
+refs:
+  - zb: "0837.55001"
+    name: Cellular structures in topology (Fritsch,Piccinini)
+---
+
+See Theorem 1.3.5 in {{zb:0837.55001}}.
diff --git a/theorems/T000886.md b/theorems/T000886.md
new file mode 100644
index 000000000..b94ebb25f
--- /dev/null
+++ b/theorems/T000886.md
@@ -0,0 +1,9 @@
+---
+uid: T000886
+if:
+  P000240: true
+then:
+  P000141: true
+---
+
+See Proposition 3.3 in <https://ncatlab.org/nlab/show/CW+complex>.