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.
Smash product of based spaces
Definition
Let and be based CGWH spaces. Their wedge inside the k-product is
The smash product is the based, kified quotient
based at the collapsed wedge. If is the quotient map, then the quotient universal property says that a based map is equivalently a continuous map that is constant with value on . The kification does not change this test against a CGWH target.
We write for . No claim that is well-pointed is made without further hypotheses.
Depends on
Compactly generated based spaces and well-pointed objects
Compact-test exponential law and products of quotient maps
For a quotient map , a map out of is continuous iff its composite with is; a continuous map on constant on the fibres of factors uniquely through ; and a composite of quotient maps is a quotient map