Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-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.

Jordan content is finitely additive when the overlap has content zero

Statement

If bounded Jordan measurable sets E,FE,F have EFE\cap F of content zero, then cont(EF)=cont(E)+cont(F).\operatorname{cont}(E\cup F)=\operatorname{cont}(E)+\operatorname{cont}(F). In particular Jordan content is additive on disjoint finite families.

Facts & Assumptions

Given: E,FE,F as stated.

[L3]

Content zero means that for every positive ε\varepsilon there is a finite cube cover of total volume below ε\varepsilon (Measure zero and content zero in Rm\mathbb{R}^m by countable and finite cube covers); Jordan inner and outer content are the inscribed supremum and covering infimum (Jordan inner and outer content and Jordan measurable bounded sets in Rm\mathbb{R}^m).

Proof

technique · induction
1.1

Pointwise, 1EF=1E+1F1EF1_{E\cup F}=1_E+1_F-1_{E\cap F}. Cube-cover content zero makes the Jordan outer content of EFE\cap F at most every positive ε\varepsilon, hence zero; its nonnegative inner content is no larger, so it too is zero. Thus EFE\cap F is Jordan measurable with content zero, and [L1] gives 1EF=0\int1_{E\cap F}=0.

L1L3given
1.2

The finite-family formula is immediate for a family of length one.

base
1.3

Assume it holds for a disjoint family of length rr.

ih
2.1

Integrate and apply [L2] to obtain the two-set formula.

step 1.1L2given
3.1

Apply the two-set formula to the union of that family and the next set. Their intersection is empty, so this adds the next content and proves the formula at length r+1r+1.

step 2.1step 1.3
4.1

Hence Jordan content is additive on every finite disjoint family.

step 1.2step 3.1discharge-induction

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 98 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources