How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A nonempty space is contractible if and only if its identity map is nullhomotopic
Statement
For a nonempty topological space , the following are equivalent:
- is contractible.
- The identity map is nullhomotopic.
Facts & Assumptions
Given: A nonempty topological space .
is contractible when every continuous map from to every topological space is nullhomotopic; a map is nullhomotopic when it is homotopic to a constant map (Nullhomotopic maps and contractible spaces).
Postcomposition by a continuous map preserves homotopies (Precomposition and postcomposition by continuous maps preserve homotopies, including their relative form, claim 2).
Proof
If is contractible, apply [A1] to the continuous map to conclude that is nullhomotopic.
Conversely suppose for some , and let be any continuous map. Postcomposition by gives by [L1]. Thus is nullhomotopic.
Since and in step 1.2 were arbitrary, every continuous map out of is nullhomotopic, so is contractible by [A1]. Together with step 1.1 this proves the equivalence.
Depends on
Used by
- Every nonempty contractible space is path-connected Corollary
- Every nonempty convex subset of ℝⁿ is contractible Corollary
- Every nonempty retract of a contractible space is contractible Corollary
- FALSE: every retract is a deformation retract False statement
- FALSE: homotopy-equivalent spaces must be homeomorphic False statement
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 23 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- A. Hatcher, Algebraic Topology, Section 0 (standard reference, not scraped)