ExampleConstruction: Literature-sourcedVerification: 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.

The Dirichlet function satisfies Lusin's conclusion without being continuous anywhere

Example

Let $D : = 1_{Q \cap [0, 1]}$ on $[0, 1]$ . Then for every $ε > 0$ there is a closed set $F \subseteq [0, 1]$ with $λ ([0, 1] ∖ F) < ε$ such that $D ∣_{F}$ is continuous, even though $D$ is nowhere continuous on $[0, 1]$ .

Facts & Assumptions

Given: The Dirichlet function $D : = 1_{Q \cap [0, 1]}$ and a real $ε > 0$ .

[L1]

The rationals are countable. ( $Q$ is countably infinite)

[L2]

For measurable $(E_{k})$ one has $μ (⋃_{k} E_{k}) \leq \sum_{k = 0}^{\infty} μ (E_{k})$ . (Finite and countable subadditivity of measures)

[L3]

If $A \subseteq B$ are measurable, then $λ (A) \leq λ (B)$ . (Measures are monotone)

[L4]

A set is closed when its complement is open. (Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen)

[L5]

Both the rationals and the irrationals are dense in $R$ . (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable)

Verification

technique · direct

1.1

By [L1], enumerate the rationals in $[0, 1]$ as $(q_{j})_{j \geq 1}$ . For each $j$ , choose an open interval $U_{j}$ centred at $q_{j}$ with length below $ε 2^{- j - 1}$ , and put $U : = ⋃_{j \geq 1} U_{j}$ . Then $Q \cap [0, 1] \subseteq U$ , and [L2] gives $λ (U) \leq \sum_{j = 1}^{\infty} λ (U_{j}) < ε .$

L1L2choose

2.1

Put $F : = [0, 1] ∖ U$ . Since $U$ is open, [L4] makes $F$ closed, and $F$ contains no rationals. Therefore $D ∣_{F} = 0$ , so the restriction is continuous. Also $[0, 1] ∖ F = U \cap [0, 1] \subseteq U$ , so [L3] and step 1.1 give $λ ([0, 1] ∖ F) \leq λ (U) < ε$ .

step 1.1L3L4

3.1

By [L5], every neighbourhood of every point of $[0, 1]$ meets both $Q$ and its complement, so $D$ is nowhere continuous on $[0, 1]$ . Thus step 2.1 is about the restriction $D ∣_{F}$ , not continuity of $D$ at the points of $F$ .

step 2.1L5∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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, Example 5.16 (standard reference, not scraped)