pi-base · felixpernegger · May 24, 2026 · May 24, 2026 · May 25, 2026 · prabau
diff --git a/theorems/T000893.md b/theorems/T000893.md
@@ -0,0 +1,16 @@
+---
+uid: T000893
+if:
+  and:
+  - P000240: true
+  - P000242: true
+then:
+  P000199: true
+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).
-Since {S162|P240}, $X$ is homotopy equivalent to the singleton by the [Whitehead theorem](https://en.wikipedia.org/wiki/Whitehead_theorem).
+The [Whitehead theorem](https://en.wikipedia.org/wiki/Whitehead_theorem) states that a
+[weak homotopy equivalence](https://en.wikipedia.org/wiki/Weak_equivalence_(homotopy_theory))
+from one CW complex to another is a homotopy equivalence.
+See Theorem 4.5 in {{zb:1044.55001}}.
+
+In particular, suppose $X$ is a {P240}. Let $Y$ be {S162} and let $f:X\to Y$ be the constant map to $Y$.
+If $X$ is {P242}, the map $f$ is a weak homotopy equivalence.
+Since {S162|P240}, the Whitehead theorem implies that $X$ is homotopy equivalent to $Y$; that is, $X$ is {P199}.
-Since {S162|P240}, $X$ is homotopy equivalent to the singleton by the [Whitehead theorem](https://en.wikipedia.org/wiki/Whitehead_theorem).
+The [Whitehead theorem](https://en.wikipedia.org/wiki/Whitehead_theorem) states that a
+[weak homotopy equivalence](https://en.wikipedia.org/wiki/Weak_equivalence_(homotopy_theory))
+from one CW complex to another is a homotopy equivalence.
+See Theorem 4.5 in {{zb:1044.55001}}.
+
+In particular, suppose $X$ is a {P240}. Let $Y$ be {S162} and let $f:X\to Y$ be the constant map to $Y$.
+If $X$ is {P242}, the map $f$ is a weak homotopy equivalence.
+Since {S162|P240}, the Whitehead theorem implies that $X$ is homotopy equivalent to $Y$; that is, $X$ is {P199}.