ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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 map $x \mapsto x + c (x)$ carries the Cantor set onto a compact set of Lebesgue measure $1$ inside $[0, 2]$

Example

Let $ψ (x) = x + c (x)$ . The gap $(1 / 3, 2 / 3)$ of the Cantor set is sent to $(5 / 6, 7 / 6)$ , because $c$ is constant there with value $1 / 2$ , while $ψ (0) = 0$ and $ψ (1) = 2$ . The A-page lemmas show that $ψ$ is a homeomorphism from $[0, 1]$ onto $[0, 2]$ and that $ψ [C]$ is a compact set of Lebesgue measure $1$ .

Facts & Assumptions

Given: The Cantor function $c$ and the map $ψ (x) = x + c (x)$ .

[L1]

$ψ$ is a homeomorphism from $[0, 1]$ onto $[0, 2]$ (The map $x \mapsto x + c (x)$ is a homeomorphism from $[0, 1]$ onto $[0, 2]$ ).

[L2]

The set $ψ [C]$ is compact and has Lebesgue measure $1$ (The homeomorphism $x \mapsto x + c (x)$ sends the Cantor set onto a compact set of Lebesgue measure $1$ ).

[L3]

The Cantor function is constant on every removed gap, and on $(1 / 3, 2 / 3)$ that constant value is $1 / 2$ (The Cantor function is well defined, satisfies $c (x) \leq c (y)$ whenever $x \leq y$ , is surjective onto $[0, 1]$ , and is constant on every interval removed from the Cantor set).

Verification

technique · direct

1.1

Step [L3] gives $ψ (x) = x + 1 / 2$ for $x \in (1 / 3, 2 / 3)$ , so $ψ (1 / 3) = 5 / 6$ , $ψ (2 / 3) = 7 / 6$ , and $ψ [(1 / 3, 2 / 3)] = (5 / 6, 7 / 6)$ . Also $ψ (0) = 0$ and $ψ (1) = 2$ .

L1L3algebra

2.1

These computations sit inside the global picture from [L1] and [L2]: the map is a homeomorphism of the whole interval, and the image of the Cantor set itself is the compact measure-one set obtained by removing the translated gaps.

L1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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 (UC Davis lecture notes), Example 2.22 (standard reference, not scraped)

The map x↦x+c(x)x↦x+c(x) carries the Cantor set onto a compact set of Lebesgue measure 11 inside [0,2][0,2]