LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

Finite measures agreeing on a generating pi-system and on the whole space are equal

Statement

Let $P$ be a pi-system on $X$ and let $A = σ_{X} (P)$ . If finite measures $μ$ and $ν$ on $(X, A)$ agree on $P$ and satisfy $μ (X) = ν (X)$ , then $μ = ν$ on $A$ .

The total-mass equality is separate because this library's pi-system convention does not require $X \in P$ .

Facts & Assumptions

Given: A pi-system $P$ generating $A$ , and finite measures $μ, ν$ agreeing on $P$ and on $X$ .

[L1]

A pi-system is a nonempty family closed under binary intersections and need not contain $X$ (Pi-systems).

[L2]

If a lambda-system contains a pi-system $P$ , then it contains $σ_{X} (P)$ (Dynkin's pi-lambda theorem).

[L3]

Measures are finitely and countably additive (Measures on sigma-algebras) and continuous from below (Continuity from below for measures).

[L4]

For finite measures, the value on a relative difference is obtained by subtracting the smaller-set value (Measure of a set difference when the smaller set has finite measure).

[L5]

The generated sigma-algebra is the intersection of all sigma-algebras containing the generating family (The sigma-algebra generated by a family of sets).

Proof

technique · direct

1.1givenL1

Let $D : = {A \in A : μ (A) = ν (A)}$ . Then $X \in D$ by the total-mass hypothesis and $P \subseteq D$ by the agreement hypothesis.

1.2givenL4algebra

If $A \subseteq B$ lie in $D$ , finiteness and [L4] give $μ (B ∖ A) = μ (B) - μ (A) = ν (B) - ν (A) = ν (B ∖ A)$ , so $B ∖ A \in D$ .

1.3givenL3

If $A_{n} ↑ A$ and each $A_{n} \in D$ , continuity from below gives $μ (A) = \sup_{n} μ (A_{n}) = \sup_{n} ν (A_{n}) = ν (A)$ , so $A \in D$ .

2.1step 1.1step 1.2step 1.3

Steps 1.1, 1.2 and 1.3 show that $D$ is a lambda-system containing $P$ .

3.1step 2.1L2L5∎

Dynkin's theorem gives $A = σ_{X} (P) \subseteq D$ , so $μ (A) = ν (A)$ for every $A \in A$ .

Depends on

Used by

Dependency tree · two levels

15 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

D. Pollard, A User's Guide to Measure Theoretic Probability, §10 (standard reference, not scraped)