TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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], R)$

Statement

Assume the Axiom of Dependent Choice ( $D C$ ). Then the set of continuous functions $[0, 1] \to 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], R)$ for the supremum metric.

Facts & Assumptions

Given: The Axiom of Dependent Choice ( $D C$ ); for $p, q \in 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], R)$ is a nonempty complete metric space in the supremum metric ( $C (K, 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 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 ( $D C$ ). 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]) ∖ 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 = ⋂_{p, q \geq 1} (C ([0, 1]) ∖ 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

Under Dependent Choice, nowhere differentiable functions form a residual subset of C([0,1],ℝ) Corollary

Dependency tree · two levels

26 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

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],R)