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

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: Positive integers $p, q$ and a function $f \in C ([0, 1], R)$ outside $E_{p, q}$ .

[L1]

The supremum metric measures uniform distance (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).

[L2]

The interval $[0, 1]$ is compact: every open cover has a finite subcover (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1givenconstruct

Because $f \notin E_{p, q}$ , for each $a \in [0, 1]$ some $t \in [0, 1]$ satisfies $∣ t - a ∣ < 1 / q$ and $∣ f (t) - f (a) ∣ > p ∣ t - a ∣$ . For $t \in [0, 1]$ and rational $δ > 0$ , let $V_{t, δ}$ consist of the points $a$ satisfying $∣ t - a ∣ < 1 / q$ and $∣ f (t) - f (a) ∣ > p ∣ t - a ∣ + 3 δ$ . Each $V_{t, δ}$ is relatively open by continuity of $f$ , and the whole indexed family covers $[0, 1]$ , since every strict gap exceeds $3 δ$ for some positive rational $δ$ .

2.1step 1.1L1L2algebra

By [L2], finitely many sets $V_{t_{i}, δ_{i}}$ cover $[0, 1]$ . Put $ε = \min_{i} δ_{i} > 0$ . If $h \in C ([0, 1], R)$ and $∥ h - f ∥_{\infty} < ε$ , then for each $a \in [0, 1]$ some $i$ has $a \in V_{t_{i}, δ_{i}}$ . The triangle inequality gives $∣ h (t_{i}) - h (a) ∣ \geq ∣ f (t_{i}) - f (a) ∣ - 2 ∥ h - f ∥_{\infty} > p ∣ t_{i} - a ∣ + 3 δ_{i} - 2 ε \geq p ∣ t_{i} - a ∣$ , while $∣ t_{i} - a ∣ < 1 / q$ . Thus no $a$ witnesses $h \in E_{p, q}$ .

3.1step 2.1∎

Step 2.1 shows that the uniform ball of radius $ε$ about every $f \notin E_{p, q}$ misses $E_{p, q}$ . The complement is open, so $E_{p, q}$ is closed. The cover and finite subcover make no countable witness selection.

Depends on

Used by

Dependency tree · two levels

31 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])