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

Inclusion-exclusion for a nonempty finite family of finite-measure sets

Statement

Let m≥1 be natural and let A0,…,Am−1 be measurable sets of finite measure. Then

μ(⋃i<mAi)=∑∅≠J⊆{0,…,m−1}(−1)∣J∣+1μ(⋂j∈JAj).

The finite sum on the right uses the following recursive order. For a one-index family it lists {0}. To pass from the order for the nonempty subsets of {0,…,m−1} to the order for those of {0,…,m}, retain the existing list, then append {m}, and then append the sets J∪{m} for nonempty J⊆{0,…,m−1} in that existing order. Thus the displayed formula for a family of size m uses only subsets of {0,…,m−1}. This convention fixes the sum without invoking an unproved permutation rule.

Facts & Assumptions

Given: A nonempty finite list A0,…,Am−1 of measurable sets, each of finite measure.

[L1]

For measurable A,B, μ(A∪B)+μ(A∩B)=μ(A)+μ(B) (The two-set measure identity μ(A∪B)+μ(A∩B)=μ(A)+μ(B)).

[L2]

The measure of a finite union is at most the sum of the member measures (Finite and countable subadditivity of measures).

[L3]

Finite sums start with the empty sum and satisfy additivity, splitting, and telescoping laws (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L4]

Natural powers satisfy a0=1 and an+1=ana (Integer powers am).

[L5]

A property true at 0 and inherited by successors holds for every natural number (The principle of mathematical induction).

Proof

technique · induction
1.1givenL5

Let P(r) be the displayed inclusion-exclusion formula for a list of r+1 finite-measure measurable sets. It suffices to prove P(r) for every r∈N.

1.2baseL3L4

For r=0, both sides of P(0) are μ(A0), since the only nonempty subset of {0} is {0} and (−1)2=1.

1.3ih

Fix r and assume P(r) for every list of r+1 such sets.

2.1givenstep 1.3L1L2algebra

Put U=⋃i<r+1Ai. By [L2], μ(U)<+∞, and [L1] applied to U and Ar+1 gives μ(U∪Ar+1)=μ(U)+μ(Ar+1)−μ(U∩Ar+1) in R.

2.2givenstep 1.3L2L3

The induction hypothesis expands μ(U) over the nonempty subsets of {0,…,r} and expands μ(U∩Ar+1)=μ(⋃i<r+1(Ai∩Ar+1)) over the same subsets; all intersections remain finite-measure.

3.1step 2.1step 2.2L3L4

In step 2.1, the terms from μ(U) are indexed by nonempty subsets not containing r+1, the term μ(Ar+1) is indexed by {r+1}, and the negated terms from step 2.2 are indexed in the stated recursive order by the sets J∪{r+1} and acquire the sign (−1)∣J∣+2=(−1)∣J∪{r+1}∣+1. Finite-sum splitting therefore gives P(r+1).

4.1step 1.1step 1.2step 2.1step 3.1L5discharge-induction∎

By induction, P(r) holds for every r, hence the stated formula holds for every nonempty finite family; the one-set boundary is step 1.2, and finiteness was used exactly in step 2.1 to permit subtraction.

Depends on

Used by

Dependency tree · two levels

30 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