CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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, F$ have $E \cap F$ of content zero, then $cont (E \cup F) = cont (E) + cont (F) .$ In particular Jordan content is additive on disjoint finite families.

Facts & Assumptions

Given: $E, F$ as stated.

[L1]

Indicator integrals equal Jordan content (A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content).

[L2]

The integral is linear (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ).

[L3]

Content zero means that for every positive $ε$ there is a finite cube cover of total volume below $ε$ (Measure zero and content zero in $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 $R^{m}$ ).

Proof

technique · induction

1.1L1L3given

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

1.2base

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

1.3ih

Assume it holds for a disjoint family of length $r$ .

2.1step 1.1L2given

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

3.1step 2.1step 1.3

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 + 1$ .

Jordan content is finitely additive when the overlap has content zero

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources