CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)

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, nowhere differentiable functions form a residual subset of $C ([0, 1], R)$

Statement

Assume Dependent Choice. The nowhere differentiable functions form a residual subset of $C ([0, 1], R)$ with the uniform metric, where differentiability at an endpoint means the corresponding one-sided derivative.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Let $X$ be a topological space and let $A \subseteq X$ . The set $A$ is nowhere dense when $int (\overline{A}) = \emptyset$ (def-interior-closure-boundary-top). It is meagre when there is a sequence $(N_{n})_{n \in N}$ of nowhere dense subsets of $X$ with $A \subseteq ⋃_{n} N_{n}$ . It is residual, or comeagre, when $X ∖ A$ is meagre. The empty union shows that $\emptyset$ is meagre, including when $X = \emptyset$ . (Nowhere dense, meagre, residual, and comeagre subsets of a topological space).

[F2]

For $p, q \in N_{> 0}$ , let $E_{p, q}$ be the functions $f \in C ([0, 1], R)$ for which some $a \in [0, 1]$ satisfies $∣ f (t) - f (a) ∣ \leq p ∣ t - a ∣$ whenever $t \in [0, 1]$ and $∣ t - a ∣ < 1 / q$ . Then $E_{p, q}$ is closed in the supremum metric. (Functions satisfying a fixed local Lipschitz bound somewhere form a closed subset of $C ([0, 1])$ ).

[F3]

For every $f \in C ([0, 1], R)$ , every $ε > 0$ , and every $M > 0$ , there is a piecewise-affine $h$ with finitely many vertices such that $∥ f - h ∥_{\infty} < ε$ and every slope on a nonvertex affine piece has absolute value greater than $M$ . (Polygonal functions with sufficiently steep nonvertex slopes are dense in $C ([0, 1])$ ).

[F4]

The pairs of natural numbers have a specified countable enumeration ( $N \times N \approx N$ ).

Proof

technique · direct

1.1F2F3F1

Fix positive integers $p, q$ . By the now choice-free proof of [F2], $E_{p, q}$ is closed. Given any uniform open ball, [F3] supplies within it a polygonal function $h$ whose slopes on all nonvertex pieces have absolute value greater than $p$ . At any $a \in [0, 1]$ , at least one side of $a$ contains arbitrarily close points on one such affine piece; the corresponding difference quotients have absolute value greater than $p$ . Hence $h \notin E_{p, q}$ . Every open ball meets the complement of $E_{p, q}$ , so $E_{p, q}$ has empty interior and is nowhere dense.

2.1step 1.1F1F2F4

Enumerate the positive-integer pairs $(p, q)$ using [F4], and let $M = ⋃_{p, q \geq 1} E_{p, q}$ . Step 1.1 and [F1] make $M$ a countable union of nowhere dense sets. If $f$ has a finite derivative at some $a$ (one-sided at an endpoint), the difference quotient is bounded near $a$ ; choose positive integers $p$ above that bound and $q$ so that $1 / q$ is within the neighborhood. Then $f \in E_{p, q}$ . Thus the complement of the set $N$ of nowhere differentiable functions is a subset of $M$ , and this same explicitly given countable family witnesses that the complement of $N$ is meagre. Hence $N$ is residual.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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

David Marker, Descriptive Set Theory, §§1–2 (standard reference, not scraped)
Michael Kunzinger, General Topology, §§11.3–11.4 (standard reference, not scraped)
MFF General Topology course summary, §4.3 (standard reference, not scraped)

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