TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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.

Under Dependent Choice, continuous nowhere differentiable functions form a dense subset of $C([0,1],\mathbb R)$

Statement

Assume the Axiom of Dependent Choice ( $\mathrm{DC}$ ). Then the set of continuous functions $[0,1]\to\mathbb R$ having no finite two-sided derivative at an interior point and no finite one-sided derivative at either endpoint is dense in $C([0,1],\mathbb R)$ for the supremum metric.

Facts & Assumptions

Given: The Axiom of Dependent Choice ( $\mathrm{DC}$ ); for $p,q\in\mathbb N_{>0}$ , $E_{p,q}$ is the fixed local-Lipschitz set of Functions satisfying a fixed local Lipschitz bound somewhere form a closed subset of $C([0,1])$ .

[L1]

Each $E_{p,q}$ is closed (Functions satisfying a fixed local Lipschitz bound somewhere form a closed subset of $C([0,1])$ ).

[L2]

Polygonal functions whose nonvertex slopes exceed any prescribed bound are dense (Polygonal functions with sufficiently steep nonvertex slopes are dense in $C([0,1])$ ).

[L3]

$C([0,1],\mathbb R)$ is a nonempty complete metric space in the supremum metric ( $C(K,\mathbb{R})$ is complete in the supremum metric for every nonempty compact metric space $K$ ).

[L4]

A finite derivative is the limit of its local difference quotients, with the stated one-sided endpoint convention (The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L5]

Assume the Axiom of Dependent Choice ( $\mathrm{DC}$ ). The intersection of countably many open dense subsets of a nonempty complete metric space is dense (Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior).

Proof

technique · direct

1.1

Each $E_{p,q}$ has empty interior. Indeed, every supremum ball contains by [L2] a polygonal $h$ all of whose nonvertex slopes have absolute value greater than $p$ ; at any point, including a vertex or endpoint, a sufficiently nearby point on an adjacent affine piece violates the defining $p$ -bound.

L2givenalgebra

1.2

If $f\in G$ had a finite derivative at $a$ , [L4] would bound its difference quotients by some integer $p$ on a sufficiently small radius $1/q$ , placing $f$ in $E_{p,q}$ ; this contradicts $f\in G$ .

L4givenalgebra

2.1

Hence every $C([0,1])\setminus E_{p,q}$ is open and dense by [L1].

L1step 1.1algebra

3.1

Apply [L5] to the complete space of [L3]. The intersection $G=\bigcap_{p,q\ge1}(C([0,1])\setminus E_{p,q})$ is dense.

L3step 2.1L5

4.1

Thus $G$ is a dense subset of the continuous nowhere-differentiable functions, which proves the statement.

step 3.1step 1.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 79 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

A generic continuous function is nowhere differentiable (standard reference, not scraped)

Under Dependent Choice, continuous nowhere differentiable functions form a dense subset of C([0,1],R)C([0,1],\mathbb R)C([0,1],R)