Weakly contractible definition + trivial theorems

properties/P000242.md

@@ -0,0 +1,28 @@
+---
+uid: P000242
+name: Weakly contractible
+aliases:
+  - Homotopically trivial
+refs:
+  - wikipedia: Weakly_contractible_space
+    name: Weakly contractible space on Wikipedia
+  - wikipedia: Weak equivalence (homotopy theory)
+    name: Weak equivalence on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+  - zb: "0979.55010"
+    name: On the Universal Space for Group Actions with Compact Isotropy (Lück, Meintrup)
+---
+
+For each integer $n\ge 0$ every continuous map $S^n\to X$ is homotopic to a constant map.
+
+$X$ is nonempty, {P37} and all [homotopy groups](https://en.wikipedia.org/wiki/Homotopy_group) $\pi_n(X)$ with $n\ge 1$ are trivial.
+In other words, $X$ is [weakly homotopy equivalent](https://en.wikipedia.org/wiki/Weak_equivalence_(homotopy_theory)) to {S162}.
+
+Defined on page 2 in {{zb:0979.55010}}.
+
+----
+#### Meta-properties
+
+- This property is preserved by homotopy equivalences.
+- This property is preserved by finite products. (See Proposition 4.2 in {{zb:1044.55001}})

theorems/T000890.md

@@ -0,0 +1,9 @@
+---
+uid: T000890
+if:
+  P000242: true
+then:
+  P000037: true
+---
+
+By definition.

theorems/T000891.md

@@ -0,0 +1,9 @@
+---
+uid: T000891
+if:
+  P000242: true
+then:
+  P000137: false
+---
+
+By definition.

theorems/T000892.md

@@ -0,0 +1,9 @@
+---
+uid: T000892
+if:
+  P000199: true
+then:
+  P000242: true
+---
+
+Follows since any homotopy equivalence is also a weak homotopy equivalence.

theorems/T000893.md

@@ -0,0 +1,9 @@
+---
+uid: T000893
+if:
+  P000242: true
+then:
+  P000200: true
+---
+
+By definition, since the first homotopy group is the fundamental group.