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 C^1 diffeomorphism maps Lebesgue null sets to Lebesgue null sets
Statement
Assume the Axiom of Countable Choice . Let be open and let be a diffeomorphism. If is Lebesgue null, then is Lebesgue null.
Facts & Assumptions
Given: Countable Choice, open sets , a diffeomorphism , and a Lebesgue null set .
Lipschitz self-maps of Euclidean space send closed-cube-cover null sets to closed-cube-cover null sets (A Lipschitz map sends null sets to null sets).
Under Countable Choice, a subset of is Lebesgue null exactly when it is null in this closed-cube-cover sense (A subset of has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers, The Axiom of Countable Choice ()).
Lebesgue measure is countably subadditive (Finite and countable subadditivity of measures).
The rational closed cubes of positive side length lying in form a countable family and their interiors cover ( is countably infinite). For each such cube , continuity of bounds its derivative on the compact convex cube, so the mean-value inequality makes Lipschitz. The coordinatewise clamp is -Lipschitz; hence is a global Lipschitz extension agreeing with on . These formulas define the extensions from the cubes without a countable selection.
Proof
Enumerate the rational cubes of [A1] as and write . By [L2], each is closed-cube-cover null. The global Lipschitz extension from [A1] agrees with on , so [L1] makes closed-cube-cover null. Applying [L2] again shows that each image is Lebesgue null.
Since , [L3] implies Hence is Lebesgue null.
Depends on
Continuously differentiable maps, local inverses, and local diffeomorphisms
A Lipschitz map sends null sets to null sets
A subset of has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers
Finite and countable subadditivity of measures
The Axiom of Countable Choice ()
is countably infinite