CorollaryStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

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.

A nonnegative integral over a null set vanishes

Statement

Let $f : X \to [0, + \infty]$ be measurable and let $E$ be measurable with $μ (E) = 0$ . Then $\int_{E} f d μ = 0.$

Facts & Assumptions

Given: A nonnegative measurable function $f$ and a measurable null set $E$ .

[L1]

The set function $A \mapsto \int_{A} s d μ$ is a measure whenever $s$ is nonnegative simple (The indefinite integral of a nonnegative simple function is a measure).

[L2]

The integral over a measurable set is defined by $\int_{E} f d μ = \int f χ_{E} d μ$ (Integral over a measurable subset).

[L3]

The nonnegative integral is the supremum of the integrals of simple minorants (The nonnegative Lebesgue integral).

Proof

technique · direct

1.1

Let $s = \sum_{j} c_{j} χ_{A_{j}}$ be a simple minorant of $f χ_{E}$ . If $c_{j} > 0$ ,[L1, L2, given] then $A_{j} \subseteq E$ , so $μ (A_{j}) = 0$ . Since $A \mapsto \int_{A} s d μ$ is a measure by [L1], every positive-coefficient term contributes $0$ , and the zero-coefficient terms contribute $0$ as well. Hence $\int s d μ = 0$ .

2.1

Taking the supremum over all such simple minorants in [L3] gives[step 1.1, L2, L3] ∎ $\int_{E} f d μ = \int f χ_{E} d μ = 0.$

Depends on

Used by

Dependency tree · two levels

11 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

Richard F. Bass, Real Analysis for Graduate Students, Proposition 6.3(4) (standard reference, not scraped)