Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

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

Statement

Let n1 and assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). For every subset ERn, measurable or not,

λn(E)  =  inf{λn(U)  :  URn open and EU},

the infimum being taken in [0,+] over a family that is nonempty because Rn is open.

Facts & Assumptions

Given: A natural number n1, the Axiom of Countable Choice, and a subset ERn.

[L1]

λn(E):=inf{k=0μ0(Ak):AkEn for every k and EkAk} (Lebesgue outer measure on Rn, Elementary sets: the finite unions of half-open boxes in Rn).

[L2]

Assuming countable choice, λn is an outer measure on Rn, hence monotone and countably subadditive, and λn(A)=μ0(A) for every elementary set A (Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume, Outer measures).

[L3]

Assuming countable choice, L(Rn) is a sigma-algebra and λn is a complete measure on it (Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume).

[L4]

Assuming countable choice, every Borel subset of Rn is Lebesgue measurable; in particular every open set is (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable).

[L5]

A+δ is an elementary set determined by A and δ alone, it contains A, and every point of A is an interior point of A+δ; and for every real ε>0 there is mN with μ0(A+1/(m+1))μ0(A)+ε (Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it, claims 1 and 2).

[F2]

The nonnegative extended sum of a sequence in [0,+] is k=0ak:=supnNsn, the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line).

[F3]

Every nonempty subset SN has a least element (The well-ordering principle).

[F4]

If r<1 then k=0rk=1/(1r); in particular k=02k=2 (For r<1, k0rk=1/(1r), and for r1 the series diverges).

[F5]

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

[F6]

The Axiom of Countable Choice says that for every family (Xn)nN of nonempty sets indexed by N there is a function f with domain N such that f(n)Xn for every nN (The Axiom of Countable Choice (ACω)).

Proof

technique · direct
1.1

Every open U is Lebesgue measurable with λn(U)=λn(U), so monotonicity of the outer measure gives λn(E)λn(U) for every open UE, and therefore λn(E) is a lower bound of the family whose infimum is displayed; that family is nonempty since Rn is open.

L2L3L4F1
1.2

Suppose λn(E)<+ and let ε be a positive real; by the definition of λn as an infimum there is a sequence (Ak)kN of elementary sets with EkAk and k=0μ0(Ak)λn(E)+ε.

L1
2.1

For each k let mk be the least natural number with μ0(Ak+1/(mk+1))μ0(Ak)+ε2k, which exists because that set of naturals is nonempty and N is well ordered, and put Uk:=int(Ak+1/(mk+1)); each Uk is open and contains Ak, so U:=kUk is open and contains E.

step 1.2L5F1F3
3.1

Countable subadditivity, monotonicity and the agreement of λn with μ0 on elementary sets give λn(U)k=0λn(Uk)k=0μ0(Ak+1/(mk+1)); every partial sum of the last series is at most k<Nμ0(Ak)+εk<N2kk=0μ0(Ak)+2ε, so the series itself, being the supremum of its partial sums, is at most λn(E)+3ε.

step 1.2step 2.1L2L5L6F2F4F5
4.1

So when λn(E)<+ the infimum is at most λn(E)+3ε for every positive real ε and hence at most λn(E); when λn(E)=+ the infimum is at most + for the same reason of triviality; with step 1.1 the infimum equals λn(E) in both cases.

step 1.1step 3.1F6

Depends on

Used by

Dependency tree · two levels

87 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