TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 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.

On a complete measure space, equality almost everywhere preserves measurability

Statement

Let $(X, A, μ)$ be a complete measure space, let $f : X \to \overline{R}$ be measurable, and let $g : X \to \overline{R}$ satisfy $g = f$ almost everywhere. Then $g$ is measurable.

Facts & Assumptions

Given: A complete measure space $(X, A, μ)$ , a measurable function $f : X \to \overline{R}$ , a function $g : X \to \overline{R}$ , and a measurable null set $N$ such that $f = g$ on $X ∖ N$ .

[L1]

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

[L2]

Threshold measurability characterizes measurable $\overline{R}$ -valued functions. (Threshold characterisations of real-valued and extended-real-valued measurability)

Proof

technique · direct

1.1

Fix a real $a$ . On $X ∖ N$ , the equality $g = f$ gives

givenalgebra

${g > a} \cap (X ∖ N) = {f > a} \cap (X ∖ N) .$

Therefore

${g > a} = ({f > a} \cap (X ∖ N)) \cup ({g > a} \cap N) .$

[given, algebra]

2.1

The set ${f > a}$ is measurable by [L2]. The set ${g > a} \cap N$ is a [step 1.1, L1, L2] subset of the measurable null set $N$ , so [L1] makes it measurable. Hence ${g > a}$ is measurable for every real $a$ .

step 1.1L1L2

3.1

By [L2], step 2.1 proves that $g$ is measurable.

step 2.1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

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

John K. Hunter, Measure Theory, Section 3.5 (standard reference, not scraped)