LemmaStatement: 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.

Functions satisfying a fixed local Lipschitz bound somewhere form a closed subset of $C([0,1])$

Statement

For $p,q\in\mathbb N_{>0}$ , let $E_{p,q}$ be the functions $f\in C([0,1],\mathbb R)$ for which some $a\in[0,1]$ satisfies $|f(t)-f(a)|\le p|t-a|$ whenever $t\in[0,1]$ and $|t-a|<1/q$ . Then $E_{p,q}$ is closed in the supremum metric.

Facts & Assumptions

Given: $f_n\in E_{p,q}$ converges to $f$ in the supremum metric.

[L1]

Supremum-metric convergence is uniform convergence (The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set, Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$ , Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions).

[L2]

Every sequence in $[0,1]$ has a convergent subsequence with limit in $[0,1]$ (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence, Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

[L3]

A uniform limit of continuous real functions is continuous (The uniform limit of continuous real-valued functions on a metric space is continuous).

Proof

technique · sequential

1.1

For each $n$ , choose a witness $a_n\in[0,1]$ for $f_n\in E_{p,q}$ . Pass to a subsequence with $a_n\to a\in[0,1]$ using [L2].

givenL2choose

1.2

By [L1], $f_n\to f$ uniformly, and [L3] confirms that $f\in C([0,1],\mathbb R)$ .

L1L3algebra

2.1

Fix $t\in[0,1]$ with $|t-a|<1/q$ . For all sufficiently large $n$ , $|t-a_n|<1/q$ , hence $|f_n(t)-f_n(a_n)|\le p|t-a_n|$ .

step 1.1givenalgebra

3.1

Letting $n$ tend to infinity in step 2.1, uniform convergence and continuity of $f$ give $|f(t)-f(a)|\le p|t-a|$ .

step 1.1step 1.2step 2.1algebra

4.1

The point $a$ witnesses $f\in E_{p,q}$ ; therefore $E_{p,q}$ is sequentially closed, hence closed in this metric space.

step 3.1L1algebra∎

Depends on

Used by

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

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 81 results over 14 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)

Functions satisfying a fixed local Lipschitz bound somewhere form a closed subset of C([0,1])C([0,1])C([0,1])