LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The completed measure is independent of the representing measurable set

Statement

If $E = A \cup N = B \cup M$ are two representations in the completion domain, with $N \subseteq Z$ , $M \subseteq W$ , and $Z, W$ measurable null sets, then $μ (A) = μ (B)$ . Consequently $\overline{μ} (E) : = μ (A)$ is well defined.

Facts & Assumptions

Given: Representations $E = A \cup N = B \cup M$ as in the Statement.

[L1]

A completed set is represented by a measurable core together with a subset of a measurable null set (The completion domain and proposed completed set function of a measure space).

[L2]

Measurable sets whose symmetric difference is null have equal measure, including at $+ \infty$ (Sets whose symmetric difference is null have the same measure).

[L3]

In every measure space, a countable union of measurable null sets is measurable and null, and every measurable subset of a null set is null (Null sets are closed under countable unions and, in a complete space, under arbitrary subsets).

Proof

technique · direct

1.1

If $x \in A ∖ B$ , then $x \in E = B \cup M$ forces $x \in M \subseteq W$ ; similarly $B ∖ A \subseteq Z$ . Hence $A △ B \subseteq Z \cup W$ .

givenL1

1.2

The measurable set $Z \cup W$ is null, and the measurable subset $A △ B$ is therefore null.

givenL3

2.1

By [L2], $μ (A) = μ (B)$ ; this also covers empty null envelopes and the case in which the common value is $+ \infty$ , so the proposed value $\overline{μ} (E)$ is independent of every representation.

step 1.1step 1.2L2∎

Depends on

Used by

Assuming countable choice, every measure space has a unique complete extension to its completion Theorem

Cited to discharge well-definedness by The completion domain and proposed completed set function of a measure space.

Dependency tree · two levels

9 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

G. Folland, Real Analysis, 2nd ed., Theorem 1.9 (standard reference, not scraped)