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 finite-measure measurable set in has a compact core and a bounded open neighbourhood of arbitrarily small excess
Statement
Assume the Axiom of Countable Choice.
Let be Lebesgue measurable with . For every there exist a compact set and a bounded open set such that
Facts & Assumptions
Given: The Axiom of Countable Choice, , a finite-measure measurable set , and .
Outer regularity gives open supersets of arbitrarily small excess (Assuming countable choice, the Lebesgue outer measure of an arbitrary subset of is the infimum of the measures of the open sets containing it).
Lebesgue measure is sigma-finite and finite on bounded sets (Lebesgue measure is sigma-finite, and every metrically bounded subset of has finite outer measure).
Continuity from below applies to the exhaustion (Continuity from below for measures).
Set-difference measure obeys the usual subtraction and monotonicity rules (Measure of a set difference when the smaller set has finite measure, Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
Proof
By [L3], choose so large that [L2, L3, given, choose] Put . Then has finite measure and lies in a compact ball.
Apply [L1] to choose an open set with [L1, L4, step 1.1, choose, construct] . Put Then is bounded and open, and it still contains because . Next choose an open set with Define Then and is compact, being closed in the compact ball .
Because , one has [step 1.1, step 2.1, L4, algebra] Also so
Since , one also has [step 2.1, L4, algebra] But , so Thus , , and both required excess bounds hold.
Depends on
Assuming countable choice, the Lebesgue outer measure of an arbitrary subset of is the infimum of the measures of the open sets containing it
Continuity from below for measures
Lebesgue measure is sigma-finite, and every metrically bounded subset of has finite outer measure
Measure of a set difference when the smaller set has finite measure
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line