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

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.

Assuming countable choice and dependent choice, a measurable function on a finite-measure subset of R^n agrees there, off a small set, with a continuous function on R^n

Statement

Assume the Axiom of Countable Choice and the Axiom of Dependent Choice. Let $n \geq 1$ , let $E \subseteq R^{n}$ be Lebesgue measurable with $λ_{n} (E) < + \infty$ , and let $f : E \to R$ be measurable. Then for every $ε > 0$ there are a continuous function $g : R^{n} \to R$ and a closed set $F \subseteq E$ such that $λ_{n} (E ∖ F) < ε and g (x) = f (x) for every x \in F .$

In particular, $λ_{n} ({x \in E : g (x) \neq f (x)}) < ε .$

Facts & Assumptions

Given: The Axiom of Countable Choice, dependent choice, a measurable function $f : E \to R$ on a finite-measure Lebesgue set $E \subseteq R^{n}$ , and a real $ε > 0$ .

[L1]

Assuming countable choice, Lusin's theorem gives a real $M > 0$ and a closed set $F \subseteq E \cap f^{- 1} ([- M, M])$ such that $λ_{n} (E ∖ F) < ε$ and $f ∣_{F}$ is continuous. (Assuming countable choice, Lusin's theorem on finite-measure subsets of R^n)

[L2]

Assuming dependent choice, every continuous map from a closed subspace of a normal space into a closed interval $[a, b]$ extends continuously to the whole space. (Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality)

[L3]

For $n \geq 1$ , $R^{n}$ carries its Euclidean metric. ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it)

[L4]

Every metric space is normal. (In a metric space any two separated sets have disjoint open neighbourhoods, so every metrizable space is completely normal)

Proof

technique · direct

1.1

By [L1], choose $M > 0$ and a closed set $F \subseteq E \cap f^{- 1} ([- M, M])$ with $λ_{n} (E ∖ F) < ε$ such that $f ∣_{F} : F \to [- M, M]$ is continuous.

L1choose

2.1

By [L3], $R^{n}$ is a metric space, so [L4] makes it normal. Apply [L2] to the closed subspace $F \subseteq R^{n}$ and to the interval $[- M, M]$ . This gives a continuous function $g : R^{n} \to [- M, M]$ with $g ∣_{F} = f ∣_{F}$ .

step 1.1L2L3L4

3.1

Since $g = f$ on $F$ , one has ${x \in E : g (x) \neq f (x)} \subseteq E ∖ F$ . Therefore $λ_{n} ({x \in E : g (x) \neq f (x)}) < ε$ . The function $g$ and the closed set $F$ satisfy the corollary.

step 1.1step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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, Theorem 5.15 (standard reference, not scraped)