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.
Euclidean balls have positive finite Lebesgue measure
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()).
Let , let , and let . Then the Euclidean ball is Lebesgue measurable and satisfies
Facts & Assumptions
Given: The Axiom of Countable Choice, an integer , a point , and a real radius .
The Euclidean ball is . (Open ball, closed ball and sphere in a metric space, as the set of functions , and , , are metrics on it)
Every box between its open and closed forms is Lebesgue measurable with its usual volume. (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
Open balls in any metric space are open; the Euclidean distance is a metric on for . (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, clause 1; as the set of functions , and , , are metrics on it)
Under Countable Choice, every Borel subset of , in particular every open subset, is Lebesgue measurable. (Assuming countable choice, every Borel subset of is Lebesgue measurable)
Under Countable Choice, is a measure on the Lebesgue sigma-algebra, and measures are monotone on measurable inclusions. (Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume, clause 1; Measures are monotone)
Proof
If , then [L1, algebra] so the open cube is contained in . On the other hand, implies for every coordinate, so .
The ball is open in the Euclidean metric by [L3], hence Borel and Lebesgue measurable by [L4] under the stated Countable Choice. The two cubes from step 1.1 are measurable by [L2], with measures [step 1.1, L2, L3, L4, algebra] Since lies between them, monotonicity [L5] gives
Therefore is Lebesgue measurable of positive finite measure.
Depends on
The Axiom of Countable Choice ()
Open ball, closed ball and sphere in a metric space
as the set of functions , and , , are metrics on it
Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed
Assuming countable choice, every Borel subset of is Lebesgue measurable
A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume
Measures are monotone