TheoremStatement: AI-adaptedProof: AI-adaptedSession-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 function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra

Statement

Assume the Axiom of Countable Choice. Let $(X, A_{0}, μ)$ be a measure space and let $(X, \overline{A_{0}}, \overline{μ})$ be its completion. If $f : X \to \overline{R}$ is measurable with respect to $\overline{A_{0}}$ , then there is an $A_{0}$ -measurable function $g : X \to \overline{R}$ such that $f = g$ almost everywhere.

Facts & Assumptions

Given: The Axiom of Countable Choice, a measure space $(X, A_{0}, μ)$ , its completion $(X, \overline{A_{0}}, \overline{μ})$ , and an $\overline{A_{0}}$ -measurable function $f : X \to \overline{R}$ .

[L1]

Every measurable function admits simple approximations dominated by its absolute value. (Every measurable function admits simple approximations dominated by its absolute value)

[L2]

A completed measurable set has the form $A \cup N$ with $A \in A_{0}$ and $N$ contained in a measurable null set. (The completion domain and proposed completed set function of a measure space)

[L3]

Assuming Countable Choice, the completion is a complete measure space extending the original measure, and countable unions of completed null sets are completed null sets. (Assuming countable choice, every measure space has a unique complete extension to its completion, Null sets are closed under countable unions and, in a complete space, under arbitrary subsets)

[L4]

Pointwise limsup of a sequence of measurable functions is measurable. (Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable)

Proof

technique · direct

1.1

By [L1], choose simple $\overline{A_{0}}$ -measurable functions [L1, choose] $s_{k} : X \to R$ with $∣ s_{k} ∣ \leq ∣ f ∣$ and $s_{k} (x) \to f (x)$ for every $x \in X$ . Write the canonical representation of $s_{k}$ as

$s_{k} = \sum_{j = 1}^{m_{k}} c_{k, j} 1_{E_{k, j}},$

where the $E_{k, j}$ are pairwise disjoint completed measurable level sets. [L1, choose]

1.2

For each pair $(k, j)$ , apply [L2] to $E_{k, j}$ and choose [L2, L3, choose] $A_{k, j} \in A_{0}$ together with a completed null set $N_{k, j}$ such that $E_{k, j} = A_{k, j} \cup M_{k, j}$ with $M_{k, j} \subseteq N_{k, j}$ . Because $A_{k, j} \subseteq E_{k, j}$ , the sets $A_{k, j}$ remain pairwise disjoint. Define

$t_{k} : = \sum_{j = 1}^{m_{k}} c_{k, j} 1_{A_{k, j}} .$

Then each $t_{k}$ is $A_{0}$ -measurable and simple. Let $N : = ⋃_{k, j} N_{k, j}$ . By [L3], $N$ is a completed measurable null set, and for every $x \notin N$ one has $t_{k} (x) = s_{k} (x)$ for all $k$ . [L2, L3, choose]

2.1

Define

step 1.1step 1.2L4

$g : = {lim sup}_{k \to \infty} t_{k} .$

By [L4], the function $g$ is $A_{0}$ -measurable. If $x \notin N$ , then step 1.2 gives $t_{k} (x) = s_{k} (x)$ for every $k$ , and step 1.1 gives $s_{k} (x) \to f (x)$ , so $g (x) = {lim sup}_{k} t_{k} (x) = \lim_{k} s_{k} (x) = f (x)$ . Hence $g = f$ on $X ∖ N$ . [step 1.1, step 1.2, L4]

3.1

The null set $N$ is measurable in the completion by [L3], so step 2.1 says [step 2.1, L3] exactly that $f = g$ almost everywhere. Since $g$ is $A_{0}$ -measurable, it is the required base-measurable representative.

step 2.1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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

Sheldon Axler, Measure, Integration and Real Analysis, Theorem 2.95 (standard reference, not scraped)
John K. Hunter, Measure Theory, Section 3.5 (standard reference, not scraped)