PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Elementary volume is finitely additive, monotone and finitely subadditive on the elementary algebra

Statement

Let $n \geq 1$ , let $E_{n}$ be the elementary subsets of $R^{n}$ (Elementary sets: the finite unions of half-open boxes in $R^{n}$ ) and let $μ_{0}$ be elementary volume (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition). Let $E, F \in E_{n}$ and let $E_{0}, \dots, E_{q - 1}$ be a finite list in $E_{n}$ . Then:

Finite additivity. If the $E_{j}$ are pairwise disjoint, then $μ_{0} (⋃_{j < q} E_{j}) = \sum_{j < q} μ_{0} (E_{j})$ .
Monotonicity. If $E \subseteq F$ , then $μ_{0} (E) \leq μ_{0} (F)$ .
Finite subadditivity. $μ_{0} (⋃_{j < q} E_{j}) \leq \sum_{j < q} μ_{0} (E_{j})$ .

All three hold with the value $+ \infty$ allowed, the sums being the finite sums of Series in the nonnegative extended real line.

Facts & Assumptions

Given: A natural number $n \geq 1$ , the algebra $E_{n}$ , elementary volume $μ_{0}$ , and elementary sets $E$ , $F$ and $E_{0}, \dots, E_{q - 1}$ .

[L1]

For every $n \geq 1$ , there is exactly one function $μ_{0} : E_{n} \to [0, + \infty]$ whose value at $A$ is the sum of the volumes of the members of any presentation of $A$ by a finite list of pairwise disjoint half-open boxes (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition).

[L2]

Every elementary set is the union of a finite list of pairwise disjoint half-open boxes (Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement).

[L3]

$E_{n}$ is an algebra of subsets of $R^{n}$ , it contains every half-open box, and it is closed under intersection of two members and under difference (The elementary sets form an algebra of subsets of $R^{n}$ containing every half-open box).

[L4]

A subset $E \subseteq R^{n}$ is an elementary set when there are a natural number $m$ and a list $B_{0}, \dots, B_{m - 1}$ of half-open boxes with $E = ⋃_{j < m} B_{j}$ (Elementary sets: the finite unions of half-open boxes in $R^{n}$ ).

[F1]

For sequences of reals, $\sum_{k < n} (a_{k} + b_{k}) = \sum_{k < n} a_{k} + \sum_{k < n} b_{k}$ ; if $m \leq n$ then $\sum_{k < n} a_{k} = \sum_{k < m} a_{k} + \sum_{k = m}^{n - 1} a_{k}$ ; and if $a_{k} \leq b_{k}$ whenever $0 \leq k < n$ then $\sum_{k < n} a_{k} \leq \sum_{k < n} b_{k}$ (Laws of finite sums and finite products, claims 1, 3 and 4).

[F2]

Finite sums of a sequence of reals are defined by the recursion $Σ_{0} = 0$ , $Σ_{σ (n)} = Σ_{n} + a_{n}$ (Finite sums and finite products, by recursion).

[F3]

The partial sums of a sequence in $[0, + \infty]$ are the unique sequence with $s_{0} = 0$ and $s_{n + 1} = s_{n} + a_{n}$ , and finite sums use the same recursion, $\sum_{k < n} a_{k} = s_{n}$ (Series in the nonnegative extended real line).

[F4]

For $a, b \in \overline{R}$ , $a + b : = + \infty$ when $a = + \infty$ and $b \neq - \infty$ , or $b = + \infty$ and $a \neq - \infty$ (The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined).

Proof

technique · direct

1.1F1F2F3F4

A finite sum in $[0, + \infty]$ equals $+ \infty$ exactly when one of its terms does, and otherwise is the finite sum of reals; hence such sums split over a concatenation of two lists, are monotone termwise, and satisfy $x \leq x + y$ for $x, y \in [0, + \infty]$ , since with all terms real these are the laws for finite sums of reals and otherwise both sides are $+ \infty$ .

2.1step 1.1L1L2L4

For claim 1, choose for each $j < q$ a presentation of $E_{j}$ by a finite list of pairwise disjoint half-open boxes, finitely many instantiations of an existential statement; the concatenated list presents $⋃_{j < q} E_{j}$ and its members are pairwise disjoint, boxes from different $E_{j}$ being disjoint because the $E_{j}$ are, so splitting the concatenated sum over the $q$ blocks gives $μ_{0} (⋃_{j < q} E_{j}) = \sum_{j < q} μ_{0} (E_{j})$ .

3.1step 1.1step 2.1L3

For claim 2, $F = E \cup (F ∖ E)$ is a disjoint union of two elementary sets, so claim 1 gives $μ_{0} (F) = μ_{0} (E) + μ_{0} (F ∖ E) \geq μ_{0} (E)$ .

4.1step 1.1step 2.1step 3.1L3∎

For claim 3, put $D_{j} : = E_{j} ∖ ⋃_{l < j} E_{l}$ ; each $D_{j}$ is elementary, the $D_{j}$ are pairwise disjoint with $⋃_{j < q} D_{j} = ⋃_{j < q} E_{j}$ , and $D_{j} \subseteq E_{j}$ , so claim 1 and then claim 2 termwise give $μ_{0} (⋃_{j < q} E_{j}) = \sum_{j < q} μ_{0} (D_{j}) \leq \sum_{j < q} μ_{0} (E_{j})$ , which with steps 2.1 and 3.1 is the Statement.

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

John K. Hunter, Measure Theory (UC Davis lecture notes), Chapter 2 (standard reference, not scraped)
T. Tao, An Introduction to Measure Theory (GSM 126), Section 1.1 (standard reference, not scraped)