Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26
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.

Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure

Statement

Let n≥1 and assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). For u,v∈Rn with ui≤vi for every i<n write [u,v] for the closed rectangle and V(u,v):={ x∈Rn:ui<xi<vi for every i<n } for the open box, both of size ∏i<n(vi−ui) (Axis-parallel rectangles in Rm and their volume); a closed cube of side ℓ≥0 is a set ∏i<n[ci,ci+ℓ], of size ℓ n. For E⊆Rn put

λcl(E):=inf⁡{∑k=0∞vol⁡[uk,vk]  :  E⊆⋃k[uk,vk]},λop(E):=inf⁡{∑k=0∞∏i<n(vik−uik)  :  E⊆⋃kV(uk,vk)},

λcb(E):=inf⁡{∑k=0∞ℓk n  :  E⊆⋃k∏i<n[cik, cik+ℓk]},

infima over countable covers of the stated kind, which exist because Rn is covered by the rectangles [−k1,k1], by the open boxes V(−k1,k1) and by the cubes ∏i[−k,−k+2k]. Then

λcl(E)  =  λop(E)  =  λcb(E)  =  λn∗(E).

Facts & Assumptions

Given: A natural number n≥1, the Axiom of Countable Choice, a subset E⊆Rn, and the three infima displayed in the Statement.

[L1]

λn∗(E):=inf⁡{∑k=0∞μ0(Ak):Ak∈En for every k and E⊆⋃kAk} (Lebesgue outer measure on Rn, Elementary sets: the finite unions of half-open boxes in Rn).

[L2]

B(a,b):={ x∈Rn:ai<xi≤bi  for every i<n }; a box is nonempty exactly when ai<bi for every i<n; vol⁡(∅):=0; and for a nonempty box with real parameters vol⁡(B):=∏i<n(bi−ai) (Half-open boxes in Rn and their volume).

[L3]

Assuming countable choice, λn∗(A)=μ0(A) for every elementary set A, and λn∗ is an outer measure (Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume), μ0 being the elementary volume of The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition.

[L4]

Assuming countable choice, λn∗(E)=inf⁡{λn(U):U open and E⊆U} (Assuming countable choice, the Lebesgue outer measure of an arbitrary subset of Rn is the infimum of the measures of the open sets containing it).

[L5]

Every open U⊆Rn is the union of an at most countable family of pairwise disjoint dyadic cubes (Every open subset of Rn is the union of a countable pairwise disjoint family of dyadic cubes), each of the form Qk,m={ x:mi2−k<xi≤(mi+1)2−k (i<n) } (Dyadic cubes of generation k in Rn, Integer powers am).

[L7]

Assuming countable choice, λn is a measure on the sigma-algebra L(Rn) with λn(B)=vol⁡(B) for every half-open box (Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume), so it is countably additive on pairwise disjoint measurable sequences (Measures on sigma-algebras).

[F1]

[a,b]:={x∈Rm:aj≤xj≤bj (j<m)} and vol⁡[a,b]:=∏j<m(bj−aj) (Axis-parallel rectangles in Rm and their volume).

[F2]

The nonnegative extended sum of a sequence in [0,+∞] is ∑k=0∞ak:=sup⁡n∈Nsn, the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line).

[F3]

Every nonempty subset S⊆N has a least element (The well-ordering principle).

[F4]

For every real ε>0 there is a natural number k≥1 with 1/k<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

[F5]

If ∣r∣<1 then ∑k=0∞rk=1/(1−r); in particular ∑k=0∞2−k=2 (For ∣r∣<1, ∑k≥0rk=1/(1−r), and for ∣r∣≥1 the series diverges).

[F6]

For sequences of reals, ∑k<n(ak+bk)=∑k<nak+∑k<nbk; ∑k<nλak=λ∑k<nak; if ak≤bk whenever 0≤k<n then ∑k<nak≤∑k<nbk; and ∏k<n(akbk)=(∏k<nak)(∏k<nbk) (Laws of finite sums and finite products, claims 1, 2, 4 and 6; Finite sums and finite products, by recursion).

[F7]

An at most countable family may always be presented as a sequence (Finite, countably infinite, countable, uncountable).

Proof

technique · direct
1.1F1F6

For a natural number r, reals 0≤pi≤qi (i<r) and a real V≥1 with qi≤V for every i<r, one has ∏i<rqi−∏i<rpi≤V r∑i<r(qi−pi): at r=0 both products are 1 and both sides are 0, and the passage from r to r+1 uses ∏i<r+1qi−∏i<r+1pi=qr(∏i<rqi−∏i<rpi)+(qr−pr)∏i<rpi with ∏i<rpi≤V r, so the estimate follows by induction on r.

1.2L2F1F6

For real ui≤vi one has V(u,v)⊆B(u,v)⊆[u,v] and vol⁡B(u,v)=vol⁡[u,v]=∏i<n(vi−ui), the box being empty and the product zero together when some ui=vi; moreover [u,v]⊆V(u−θ1, v+θ1) for every real θ>0, whose size is ∏i<n(vi−ui+2θ), and a closed cube of side ℓ is the closed rectangle [c,c+ℓ1] of size ℓ n.

2.1step 1.2F1

λcl(E)≤λcb(E), because every closed-cube cover is a closed-rectangle cover with the same terms.

2.2step 1.2L1L2L3

λn∗(E)≤λop(E), because an open-box cover E⊆⋃kV(uk,vk) gives the elementary cover E⊆⋃kB(uk,vk) whose covering cost ∑kμ0(B(uk,vk)) has exactly the same terms.

2.3step 1.1step 1.2F2F3F4F5F6

λop(E)≤λcl(E): given a closed-rectangle cover and a real ε>0, let mk be the least natural number with ∏i<n(vik−uik+2/(mk+1))≤vol⁡[uk,vk]+ε2−k, which exists by step 1.1 with V a real at least 1 bounding all vik−uik+2 and by the Archimedean property; the open boxes V(uk−θk1,vk+θk1) with θk:=1/(mk+1) cover E, and each partial sum of their sizes is at most ∑k<Nvol⁡[uk,vk]+ε∑k<N2−k≤∑k=0∞vol⁡[uk,vk]+2ε, so λop(E) is at most that closed cover's total plus 2ε, for every positive real ε.

2.4step 1.2L4L5L6L7F1F7

λcb(E)≤λn∗(E): the inequality is trivial when λn∗(E)=+∞, and otherwise, given a real ε>0, outer regularity supplies an open U⊇E with λn(U)≤λn∗(E)+ε, the dyadic decomposition writes U as a disjoint union of an at most countable family of dyadic cubes, presented as a sequence (Qkj,mj)j and padded with copies of ∅ if it is finite, countable additivity gives ∑jλn(Qkj,mj)=λn(U), and each Qkj,mj is contained in the closed cube ∏i<n[mij2−kj, mij2−kj+2−kj] of side 2−kj and size 2−kjn=λn(Qkj,mj), a padding term contributing the degenerate cube of side 0.

3.1step 2.1step 2.2step 2.3step 2.4∎

The four quantities therefore satisfy λcl(E)≤λcb(E)≤λn∗(E)≤λop(E)≤λcl(E), so all four are equal.

Depends on

Used by

Dependency tree · two levels

97 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