Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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, four equivalent descriptions of a Lebesgue measurable subset of Rn

Statement

Let n1, assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)) and let ERn. Then E is Lebesgue measurable (Lebesgue measurable sets, the family L(Rn), and the restricted set function λn) if and only if each of the following four conditions holds, and the four are equivalent to one another.

  1. Open excess. For every real ε>0 there is an open UE with λn(UE)<ε.
  2. Gδ minus null. There are a Gδ set G and a set Z with λn(Z)=0 and E=GZ (Gδ and Fσ subsets of a topological space, agreeing with the real-line notion).
  3. Closed deficit. For every real ε>0 there is a closed FE with λn(EF)<ε.
  4. Fσ plus null. There are an Fσ set H and a set W with λn(W)=0 and E=HW.

Each condition is stated for sets of infinite measure as well as finite ones, which is why the excess and the deficit are measured by the outer measure of a difference rather than by a difference of measures.

Facts & Assumptions

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

[L1]

Assuming countable choice, for every Lebesgue measurable E and every real ε>0 there is an open U with EU and λn(UE)<ε (For a Lebesgue measurable set and every positive ε there is an open superset whose difference from it has outer measure below ε).

[L2]

Assuming countable choice, a set admitting open supersets of arbitrarily small outer excess is GZ with G a Gδ containing it and λn(Z)=0, and is Lebesgue measurable (A subset of Rn with open supersets of arbitrarily small excess is Lebesgue measurable).

[L3]

Assuming countable choice, L(Rn) is a sigma-algebra, λn is a complete measure on it, and every S with λn(S)=0 is Lebesgue measurable of measure 0 (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 (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable).

[L5]

Assuming countable choice, λn is an outer measure on Rn, hence monotone (Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume, Outer measures).

[L6]

Assuming countable choice, λn(E)=inf{λn(U):U open and EU} (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).

[F1]

A is a Gδ set of X when there is a sequence (Vn)nN of open subsets of X with A=nNVn, and an Fσ set of X when there is a sequence (Fn)nN of closed subsets with A=nNFn (Gδ and Fσ subsets of a topological space, agreeing with the real-line notion).

[F3]

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

[F4]

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

Measurability implies condition 1, which is the cited lemma on the open excess of a measurable set.

L1
1.2

Condition 1 implies condition 2, which is the first clause of the cited lemma on small open excess.

L2
1.3

Condition 2 implies measurability: G is a countable intersection of open sets, hence Borel and measurable; Z has outer measure 0, hence is measurable; so E=GZ is measurable.

L3L4F1
1.4

Condition 4 implies measurability, by the same argument read for unions: H is a countable union of closed sets, hence Borel and measurable, W is measurable because λn(W)=0, and E=HW is measurable.

L3L4F1
2.1

Measurability implies condition 3: the complement RnE is measurable, so for a real ε>0 step 1.1 supplies an open URnE with λn(U(RnE))<ε; then F:=RnU is closed, FE, and EF=EU=U(RnE), so λn(EF)<ε.

step 1.1L3F2
3.1

Condition 3 implies condition 4: for each mN the family of closed FE with λn(EF)<1/(m+1) is nonempty, so countable choice selects such an Fm; then H:=mFm is an Fσ set with HE, and W:=EHEFm gives λn(W)1/(m+1) for every m, hence λn(W)=0 and E=HW.

step 2.1L5F1F3F4
4.1

The implications of steps 1.1, 1.2 and 1.3 close the cycle between measurability and conditions 1 and 2, and those of steps 2.1, 3.1 and 1.4 close the cycle between measurability and conditions 3 and 4; so all five statements are equivalent, and outer regularity is what stands behind the open sets produced in step 1.1.

step 1.1step 1.2step 1.3step 1.4step 2.1step 3.1L6

Depends on

Used by

Dependency tree · two levels

73 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