Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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 Rn is approximable in measure by a finite union of boxes

Statement

Assume the Axiom of Countable Choice.

Let ERn be Lebesgue measurable with λn(E)<. For every ε>0 there is a finite union of boxes B such that

λn(EB)<ε.

Facts & Assumptions

Given: The Axiom of Countable Choice, a natural number n1, a Lebesgue measurable set ERn with finite measure, and ε>0.

[L2]

Every open subset of Rn is a countable disjoint union of dyadic cubes (Every open subset of Rn is the union of a countable pairwise disjoint family of dyadic cubes).

[L3]

Continuity from below applies to increasing unions of measurable sets (Continuity from below for measures).

[L4]

Measure is monotone and λn(UF)=λn(U)λn(F) when FU and λn(U)< (Measures are monotone, Measure of a set difference when the smaller set has finite measure).

Proof

technique · direct
1.1

By [L1], choose an open set UE with [L1, L4, given, choose] λn(UE)<ε/2. Because λn(E)<, monotonicity gives λn(U)λn(E)+λn(UE)<.

L1L4givenchoose
1.2

Write U=k1Qk as a countable pairwise disjoint union [L2, L3, L4, choose] of dyadic cubes by [L2], and set Bm:=k=1mQk. Then BmU, so [L3] gives λn(Bm)λn(U). Hence for some m, λn(UBm)=λn(U)λn(Bm)<ε/2.

L2L3L4choose
2.1

Put B:=Bm. Since EU and BU, [step 1.1, step 1.2, L4, algebra] EB(UE)(UB), so λn(EB)λn(UE)+λn(UB)<ε. The set B is a finite union of boxes because each dyadic cube is a box.

step 1.1step 1.2L4algebra

Depends on

Used by

Dependency tree · two levels

41 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources