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.
On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let . Under the identification the product measure and the Euclidean Lebesgue measure agree on every Borel subset of .
Statement references
Facts & Assumptions
Given: The Axiom of Countable Choice, positive integers , and the identification .
The Borel sigma-algebra on is . (The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n})
The product measure on sigma-finite spaces exists and satisfies the rectangle formula. (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique)
Assuming countable choice, Lebesgue measure of a box is the product of its side lengths. (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
Two measures that agree on a sigma-finite generating pi-system agree on the generated sigma-algebra. (Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system)
Rational half-open boxes, together with the empty set, form a generating pi-system for . The increasing boxes exhaust the space and have finite measure for both measures in the Statement.
Proof
For , the cubes exhaust and have finite measure by [L3], so the sigma-finite product theorem [L2] applies. Let be a rational half-open box. Split it as with and . Then the rectangle formula of [L2] and [L3] give
Each from [A1] has finite -measure by [L3], and finite product measure by [L2] and [L3]; step 1.1 shows these values agree. The same step gives agreement on the whole generating pi-system, while [L1] identifies its generated sigma-algebra with . Therefore [L5] implies on every Borel set.
Depends on
The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}
For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system
Pi-systems
The Axiom of Countable Choice ()