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

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

Statement

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.

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 $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 $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], 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}) ∣ \leq 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) ∣ \leq 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

Dependency tree · two levels

34 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)

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