Alphabeta MathHow 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.
The image of a compact space lies in a finite CW subcomplex
Statement
If is compact and is continuous into a CW complex, then lies in a finite CW subcomplex of .
Facts & Assumptions
Given: A continuous map with compact.
With characteristic maps supplied, a compact CW image lies in a finite subcomplex without choice (Compact CW images have finite cell support without choice).
Proof
The characteristic maps are part of the supplied CW structure. Thus the given compact space and continuous map satisfy the hypotheses of [L1].
Apply [L1] to obtain a finite CW subcomplex containing , including the empty-image case. The supplier uses canonical coordinate minima to prove finite cell support without a choice premise.
Depends on
Used by
- The Thom prespectrum of the universal real and oriented bundles Definition
- A rational homology four-ball has square boundary torsion order Lemma
- Every bordism class is realized by an embedded collapse Lemma
- Homology of an infinite CW complex is the colimit of skeletal homology Lemma
- Oriented Grassmannians have two lifted Schubert cells Lemma
- The double cover branched over a slice disk is a rational homology ball Lemma
- The normal Pontryagin class is the rational inverse of the tangent Pontryagin class Lemma
- Products of complex projective spaces span rational oriented bordism Proposition
- The universal Pontryagin-Thom correspondence for unoriented and oriented bordism Theorem
Dependency tree · two levels
8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Allen Hatcher, Algebraic Topology, Appendix A (standard reference, not scraped)