From 2f661df9b1ee5de31c2ffdff6ef0494dd0079056 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 25 Apr 2026 20:47:51 +0200
Subject: [PATCH 01/19] cellular

---
 properties/P000007.md |  1 +
 properties/P000240.md | 18 ++++++++++++++++++
 theorems/T000883.md   | 12 ++++++++++++
 theorems/T000884.md   | 12 ++++++++++++
 4 files changed, 43 insertions(+)
 create mode 100644 properties/P000240.md
 create mode 100644 theorems/T000883.md
 create mode 100644 theorems/T000884.md

diff --git a/properties/P000007.md b/properties/P000007.md
index 66128adda5..534bf48f7d 100644
--- a/properties/P000007.md
+++ b/properties/P000007.md
@@ -4,6 +4,7 @@ name: "$T_4$"
 aliases:
   - Normal Hausdorff
   - T4
+  - Normal
 refs:
   - zb: "1052.54001"
     name: General Topology (Willard)
diff --git a/properties/P000240.md b/properties/P000240.md
new file mode 100644
index 0000000000..c8ba2664e8
--- /dev/null
+++ b/properties/P000240.md
@@ -0,0 +1,18 @@
+---
+uid: P000241
+name: Cellular
+aliases:
+  - Has a CW structure
+refs:
+  - wikipedia: CW complex
+    name: CW complex on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+$X$ is homeomorphic to the underlying space of a [CW complex](https://en.wikipedia.org/wiki/CW_complex).
+
+----
+#### 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 0000000000..5a157e1052
--- /dev/null
+++ b/theorems/T000883.md
@@ -0,0 +1,12 @@
+---
+uid: T000882
+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/T000884.md b/theorems/T000884.md
new file mode 100644
index 0000000000..4eac3e32ea
--- /dev/null
+++ b/theorems/T000884.md
@@ -0,0 +1,12 @@
+---
+uid: T000882
+if:
+  P000240: true
+then:
+  P000007: true
+refs:
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+See Proposition A.3 in {{zb:1044.55001}}, where "normal" is defined as {P7}.

From 697f6e64d0f36d2bdf220df0885ff7707f2f5e0f Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 25 Apr 2026 20:48:58 +0200
Subject: [PATCH 02/19] fix uid

---
 theorems/T000883.md | 2 +-
 theorems/T000884.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theorems/T000883.md b/theorems/T000883.md
index 5a157e1052..fe5daf2b15 100644
--- a/theorems/T000883.md
+++ b/theorems/T000883.md
@@ -1,5 +1,5 @@
 ---
-uid: T000882
+uid: T000883
 if:
   P000240: true
 then:
diff --git a/theorems/T000884.md b/theorems/T000884.md
index 4eac3e32ea..fb463eddfc 100644
--- a/theorems/T000884.md
+++ b/theorems/T000884.md
@@ -1,5 +1,5 @@
 ---
-uid: T000882
+uid: T000884
 if:
   P000240: true
 then:

From ff5634e74bedf35175d4d9108c190ba0c70ca1c0 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 25 Apr 2026 20:59:55 +0200
Subject: [PATCH 03/19] fix uid once more

---
 properties/P000240.md | 2 +-
 theorems/T000883.md   | 4 ++--
 theorems/T000884.md   | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index c8ba2664e8..69a1281b40 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -1,5 +1,5 @@
 ---
-uid: P000241
+uid: P000240
 name: Cellular
 aliases:
   - Has a CW structure
diff --git a/theorems/T000883.md b/theorems/T000883.md
index fe5daf2b15..0d11ea8ad7 100644
--- a/theorems/T000883.md
+++ b/theorems/T000883.md
@@ -3,10 +3,10 @@ uid: T000883
 if:
   P000240: true
 then:
-  P000223: true
+  P000007: true
 refs:
   - zb: "1044.55001"
     name: Algebraic Topology (Hatcher)
 ---
 
-See Proposition A.4 in {{zb:1044.55001}}.
+See Proposition A.3 in {{zb:1044.55001}}, where "normal" is defined as {P7}.
diff --git a/theorems/T000884.md b/theorems/T000884.md
index fb463eddfc..7ae33cddb0 100644
--- a/theorems/T000884.md
+++ b/theorems/T000884.md
@@ -3,10 +3,10 @@ uid: T000884
 if:
   P000240: true
 then:
-  P000007: true
+  P000223: true
 refs:
   - zb: "1044.55001"
     name: Algebraic Topology (Hatcher)
 ---
 
-See Proposition A.3 in {{zb:1044.55001}}, where "normal" is defined as {P7}.
+See Proposition A.4 in {{zb:1044.55001}}.

From 406026fb4bfa63892f08650178778da8a7335377 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 25 Apr 2026 22:17:07 +0200
Subject: [PATCH 04/19] paracompact

---
 theorems/T000885.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 theorems/T000885.md

diff --git a/theorems/T000885.md b/theorems/T000885.md
new file mode 100644
index 0000000000..0b0d7ccf48
--- /dev/null
+++ b/theorems/T000885.md
@@ -0,0 +1,12 @@
+---
+uid: T000884
+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}}.

From 38d4baf4e6a3ab52813c582b46b07511a660f6f5 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 25 Apr 2026 22:18:07 +0200
Subject: [PATCH 05/19] fix uid

---
 theorems/T000885.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000885.md b/theorems/T000885.md
index 0b0d7ccf48..ea8a01b983 100644
--- a/theorems/T000885.md
+++ b/theorems/T000885.md
@@ -1,5 +1,5 @@
 ---
-uid: T000884
+uid: T000885
 if:
   P000240: true
 then:

From 1ec2ddfcc75660706a0e7fd7ed91266f3f0ebc68 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 02:56:18 +0200
Subject: [PATCH 06/19] compactly generated

---
 theorems/T000886.md | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 theorems/T000886.md

diff --git a/theorems/T000886.md b/theorems/T000886.md
new file mode 100644
index 0000000000..b94ebb25ff
--- /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>.

From 8876bcbbf3af61c25213a1f67680eb1204d3c209 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 03:39:14 +0200
Subject: [PATCH 07/19] add def of cw complex

---
 properties/P000240.md | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index 69a1281b40..ffdae33157 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -1,8 +1,6 @@
 ---
 uid: P000240
-name: Cellular
-aliases:
-  - Has a CW structure
+name: CW complex
 refs:
   - wikipedia: CW complex
     name: CW complex on Wikipedia
@@ -10,7 +8,12 @@ refs:
     name: Algebraic Topology (Hatcher)
 ---
 
-$X$ is homeomorphic to the underlying space of a [CW complex](https://en.wikipedia.org/wiki/CW_complex).
+There exist subspaces $\empty = X_{-1}\subseteq X_0 \subseteq \dots \subseteq X$, such that:
+
+- $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-cells.
+- A subspace $U \subseteq X$ is open iff $U \cap X_n$ open in $X_n$ for all $n \geq -1$.
+
+For an alternative, categorical (and more modern) definition, see <https://ncatlab.org/nlab/show/CW+complex>.
 
 ----
 #### Meta-properties

From 43a44c3c6b1aa8efd192e015f37b38b95bf01358 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 03:46:52 +0200
Subject: [PATCH 08/19] add disclaimer

---
 properties/P000240.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/properties/P000240.md b/properties/P000240.md
index ffdae33157..f565ae53b2 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -1,6 +1,9 @@
 ---
 uid: P000240
 name: CW complex
+aliases:
+  - Cellular complex
+  - Cell complex
 refs:
   - wikipedia: CW complex
     name: CW complex on Wikipedia
@@ -13,6 +16,8 @@ There exist subspaces $\empty = X_{-1}\subseteq X_0 \subseteq \dots \subseteq X$
 - $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-cells.
 - A subspace $U \subseteq X$ is open iff $U \cap X_n$ open in $X_n$ for all $n \geq -1$.
 
+*Note:* Techincally, a CW complex is a topological space together with such a subset filtration (this is i.e. necessary to define cellular maps). For simplicity, we omit this technicality here.
+
 For an alternative, categorical (and more modern) definition, see <https://ncatlab.org/nlab/show/CW+complex>.
 
 ----

From 013675d111f00929d8eb34a75527aaa8b3350f1d Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 04:08:48 +0200
Subject: [PATCH 09/19] update to t6

---
 theorems/T000883.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theorems/T000883.md b/theorems/T000883.md
index 0d11ea8ad7..8c3f62ed8b 100644
--- a/theorems/T000883.md
+++ b/theorems/T000883.md
@@ -3,10 +3,10 @@ uid: T000883
 if:
   P000240: true
 then:
-  P000007: true
+  P000067: true
 refs:
-  - zb: "1044.55001"
-    name: Algebraic Topology (Hatcher)
+  - zb: "0207.21704"
+    name: The Topology of CW Complexes (Lundell, Weingram)
 ---
 
-See Proposition A.3 in {{zb:1044.55001}}, where "normal" is defined as {P7}.
+See Proposition 4.3 in {{zb:0207.21704}}, where "perfectly normal" is defined as {P67}.

From 39010132472446c149994c54e1b376e8b0db9fbf Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 04:22:43 +0200
Subject: [PATCH 10/19] add 1 more terms

---
 properties/P000240.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index f565ae53b2..f529a41f07 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -11,7 +11,7 @@ refs:
     name: Algebraic Topology (Hatcher)
 ---
 
-There exist subspaces $\empty = X_{-1}\subseteq X_0 \subseteq \dots \subseteq X$, such that:
+$X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subseteq \dots \subseteq X$, such that:
 
 - $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-cells.
 - A subspace $U \subseteq X$ is open iff $U \cap X_n$ open in $X_n$ for all $n \geq -1$.

From cf456fa1b064e770b16451c8d0001b8e74b6da9c Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 04:28:06 +0200
Subject: [PATCH 11/19] add union

---
 properties/P000240.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index f529a41f07..b85c3e28be 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -11,10 +11,10 @@ refs:
     name: Algebraic Topology (Hatcher)
 ---
 
-$X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subseteq \dots \subseteq X$, such that:
+$X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subseteq \dots$, such that:
 
 - $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-cells.
-- A subspace $U \subseteq X$ is open iff $U \cap X_n$ open in $X_n$ for all $n \geq -1$.
+- $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$.
 
 *Note:* Techincally, a CW complex is a topological space together with such a subset filtration (this is i.e. necessary to define cellular maps). For simplicity, we omit this technicality here.
 

From 11ac1e1e86a294b4cd321e0739ecdf5557a1df4f Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 04:37:31 +0200
Subject: [PATCH 12/19] delete aliases (why not)

---
 properties/P000240.md | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index b85c3e28be..d3ff2c3815 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -1,9 +1,6 @@
 ---
 uid: P000240
 name: CW complex
-aliases:
-  - Cellular complex
-  - Cell complex
 refs:
   - wikipedia: CW complex
     name: CW complex on Wikipedia

From a33629cda2e4836063c39b6d11aabbe91c3e0d69 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 04:38:07 +0200
Subject: [PATCH 13/19] typo

---
 properties/P000240.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index d3ff2c3815..c8e5443df7 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -13,7 +13,7 @@ $X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subsete
 - $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-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$.
 
-*Note:* Techincally, a CW complex is a topological space together with such a subset filtration (this is i.e. necessary to define cellular maps). For simplicity, we omit this technicality here.
+*Note:* Technically, a CW complex is a topological space together with such a subset filtration (this is i.e. necessary to define cellular maps). For simplicity, we omit this technicality here.
 
 For an alternative, categorical (and more modern) definition, see <https://ncatlab.org/nlab/show/CW+complex>.
 

From 9dab4694d0246de904d7c15217025b39290872c2 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 04:54:14 +0200
Subject: [PATCH 14/19] change disclaimer

---
 properties/P000240.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index c8e5443df7..22e7c0d4d5 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -13,7 +13,8 @@ $X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subsete
 - $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-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$.
 
-*Note:* Technically, a CW complex is a topological space together with such a subset filtration (this is i.e. necessary to define cellular maps). For simplicity, we omit this technicality here.
+*Note:* In standard usage, a CW complex is a topological space together with a chain of subspaces as above (this is i.e. necessary to define cellular maps).
+However, we are only concerned with the underlying topological space.
 
 For an alternative, categorical (and more modern) definition, see <https://ncatlab.org/nlab/show/CW+complex>.
 

From 209fbaf091547ffdc1cbe9d45b861d1e625d0648 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sun, 26 Apr 2026 19:04:20 +0200
Subject: [PATCH 15/19] add def attaching cells

---
 properties/P000240.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/properties/P000240.md b/properties/P000240.md
index 22e7c0d4d5..0e7f9f5c00 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -13,6 +13,8 @@ $X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subsete
 - $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-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+1)-cells* means that there is a discrete space $J$ and for every $j \in J$ a continuous map $f_j:S^n \to X_n$ such that $X_{n+1}$ is homeomorph to the quotient $(X_n \sqcup (J \times D^{n+1})) / \sim$, where $\sim$ is the equivalence relation generated by $(j,x)\sim f_j(x)$ for all $x \in J \times S^{n+1}$ (where we identify $\partial D^{n+1}$ with $S^n$).
+
 *Note:* In standard usage, a CW complex is a topological space together with a chain of subspaces as above (this is i.e. necessary to define cellular maps).
 However, we are only concerned with the underlying topological space.
 

From 5636d3f835a5d202f2f3dfdcaed9e4b726466bf5 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Mon, 27 Apr 2026 05:11:10 +0200
Subject: [PATCH 16/19] Update properties/P000007.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 properties/P000007.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/properties/P000007.md b/properties/P000007.md
index 534bf48f7d..66128adda5 100644
--- a/properties/P000007.md
+++ b/properties/P000007.md
@@ -4,7 +4,6 @@ name: "$T_4$"
 aliases:
   - Normal Hausdorff
   - T4
-  - Normal
 refs:
   - zb: "1052.54001"
     name: General Topology (Willard)

From 35c1e0faf9feae22a94576856f66a2bbc9b2d270 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Mon, 27 Apr 2026 19:47:20 +0200
Subject: [PATCH 17/19] inline S^n

---
 properties/P000240.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/properties/P000240.md b/properties/P000240.md
index 0e7f9f5c00..1b41fcd9c0 100644
--- a/properties/P000240.md
+++ b/properties/P000240.md
@@ -13,7 +13,9 @@ $X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subsete
 - $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-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+1)-cells* means that there is a discrete space $J$ and for every $j \in J$ a continuous map $f_j:S^n \to X_n$ such that $X_{n+1}$ is homeomorph to the quotient $(X_n \sqcup (J \times D^{n+1})) / \sim$, where $\sim$ is the equivalence relation generated by $(j,x)\sim f_j(x)$ for all $x \in J \times S^{n+1}$ (where we identify $\partial D^{n+1}$ with $S^n$).
+Here *attaching (n+1)-cells* means that there is a discrete space $J$ and for every $j \in J$ a continuous map $f_j:\partial D^{n+1} \to X_n$ such that $X_{n+1}$ is homeomorph to the quotient $(X_n \sqcup (J \times D^{n+1})) / \sim$, where $\sim$ is the equivalence relation generated by $(j,x)\sim f_j(x)$ for all $x \in J \times \partial D^{n+1}$.
+
+Here $D^n$ is the closed disk in $n$-dimensions and $\partial D^0 := \emptyset$.
 
 *Note:* In standard usage, a CW complex is a topological space together with a chain of subspaces as above (this is i.e. necessary to define cellular maps).
 However, we are only concerned with the underlying topological space.

From 93fa346a4526d9ef47ac556ed3978fe47fb6cfde Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Mon, 27 Apr 2026 20:41:29 +0200
Subject: [PATCH 18/19] pr

---
 properties/P000241.md | 21 +++++++++++++++++++++
 theorems/T000900.md   |  9 +++++++++
 theorems/T000901.md   |  9 +++++++++
 theorems/T000902.md   |  9 +++++++++
 theorems/T000903.md   |  9 +++++++++
 theorems/T000904.md   | 16 ++++++++++++++++
 6 files changed, 73 insertions(+)
 create mode 100644 properties/P000241.md
 create mode 100644 theorems/T000900.md
 create mode 100644 theorems/T000901.md
 create mode 100644 theorems/T000902.md
 create mode 100644 theorems/T000903.md
 create mode 100644 theorems/T000904.md

diff --git a/properties/P000241.md b/properties/P000241.md
new file mode 100644
index 0000000000..abb71a7832
--- /dev/null
+++ b/properties/P000241.md
@@ -0,0 +1,21 @@
+---
+uid: P000241
+name: Weakly contractible
+aliases:
+  - Homotopically trivial
+refs:
+  - wikipedia: Weakly_contractible_space
+    name: Weakly contractible space on Wikipedia
+  - wikipedia: Homotopy_group
+    name: Homotopy group on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+A nonempty, {P37} space for which all [homotopy groups](https://en.wikipedia.org/wiki/Homotopy_group) are trivial. Equivalently, the space is weakly homotopy equivalent to {S162}. 
+
+----
+#### Meta-properties
+
+- This property is preserved by homotopy equivalences.
+- This property is preserved by finite products. (See Proposition 4.2 in {{zb:1044.55001}})
diff --git a/theorems/T000900.md b/theorems/T000900.md
new file mode 100644
index 0000000000..1f4415c9af
--- /dev/null
+++ b/theorems/T000900.md
@@ -0,0 +1,9 @@
+---
+uid: T000900
+if:
+  P000241: true
+then:
+  P000037: true
+---
+
+By definition.
diff --git a/theorems/T000901.md b/theorems/T000901.md
new file mode 100644
index 0000000000..b8b40a87b0
--- /dev/null
+++ b/theorems/T000901.md
@@ -0,0 +1,9 @@
+---
+uid: T000901
+if:
+  P000241: true
+then:
+  P000137: false
+---
+
+By definition.
diff --git a/theorems/T000902.md b/theorems/T000902.md
new file mode 100644
index 0000000000..bb5c8f2b32
--- /dev/null
+++ b/theorems/T000902.md
@@ -0,0 +1,9 @@
+---
+uid: T000902
+if:
+  P000199: true
+then:
+  P000241: false
+---
+
+Follows since any homotopy equivalence is also a weak homotopy equivalence.
diff --git a/theorems/T000903.md b/theorems/T000903.md
new file mode 100644
index 0000000000..23afd874cd
--- /dev/null
+++ b/theorems/T000903.md
@@ -0,0 +1,9 @@
+---
+uid: T000903
+if:
+  P000241: true
+then:
+  P000200: false
+---
+
+By definition, since the first homotopy group is the fundamental group.
diff --git a/theorems/T000904.md b/theorems/T000904.md
new file mode 100644
index 0000000000..457810b830
--- /dev/null
+++ b/theorems/T000904.md
@@ -0,0 +1,16 @@
+---
+uid: T000902
+if:
+  and:
+  - P000240: true
+  - P000241: true
+then:
+  P000199: false
+refs:
+  - wikipedia: Whitehead_theorem
+    name: Whitehead theorem on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+Since {S162|P240}, $X$ is homotopy equivalent to the singleton by the [Whitehead theorem](https://en.wikipedia.org/wiki/Whitehead_theorem).

From 576fe08290ff416b9018e17a7a676440aec60f70 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Mon, 27 Apr 2026 20:41:45 +0200
Subject: [PATCH 19/19] fix uid

---
 theorems/T000904.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000904.md b/theorems/T000904.md
index 457810b830..254bb0751c 100644
--- a/theorems/T000904.md
+++ b/theorems/T000904.md
@@ -1,5 +1,5 @@
 ---
-uid: T000902
+uid: T000904
 if:
   and:
   - P000240: true