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 E⊆Rn be Lebesgue measurable with λn(E)<∞. For every ε>0 there is a finite union of boxes B such that

λn(E△B)<ε.

Facts & Assumptions

Given: The Axiom of Countable Choice, a natural number n≥1, a Lebesgue measurable set E⊆Rn 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(U∖F)=λn(U)−λn(F) when F⊆U and λn(U)<∞ (Measures are monotone, Measure of a set difference when the smaller set has finite measure).

Proof

technique · direct
1.1L1L4givenchoose

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

1.2L2L3L4choose

Write U=⨆k≥1Qk as a countable pairwise disjoint union [L2, L3, L4, choose] of dyadic cubes by [L2], and set Bm:=⋃k=1mQk. Then Bm↑U, so [L3] gives λn(Bm)→λn(U). Hence for some m, λn(U∖Bm)=λn(U)−λn(Bm)<ε/2.

2.1step 1.1step 1.2L4algebra∎

Put B:=Bm. Since E⊆U and B⊆U, [step 1.1, step 1.2, L4, algebra] E△B⊆(U∖E)∪(U∖B), so λn(E△B)≤λn(U∖E)+λn(U∖B)<ε. The set B is a finite union of boxes because each dyadic cube is a box.

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