CounterexampleConstruction: Literature-sourcedVerification: 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.

Translations of a fixed bump on $\mathbb R$ are uniformly bounded and equicontinuous but have no uniformly convergent subsequence

Statement refuted

Refuted: on an arbitrary metric domain, a uniformly bounded family satisfying the usual all-metric-space $\varepsilon$ -- $\delta$ equicontinuity condition must have a uniformly convergent subsequence.

Facts & Assumptions

Given: $b(x)=\max\{1-|x|,0\}$ and $f_n(x)=b(x-n)$ for $n\in\mathbb N$ .

[L1]

A uniformly convergent sequence of real-valued functions is uniformly Cauchy (A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy).

Proof

technique · direct

1.1

The triangular bump is $1$ -Lipschitz and takes values in $[0,1]$ . Every translate $f_n$ has the same properties. Thus the family is uniformly bounded and, for every $\varepsilon>0$ , the common choice $\delta=\varepsilon$ gives $|x-y|<\delta\Rightarrow|f_n(x)-f_n(y)|<\varepsilon$ for every $n$ ; this is the ordinary all-metric-space equicontinuity condition used in the refuted claim.

givenalgebra

1.2

If $|m-n|\ge2$ , then at $x=n$ one has $f_n(n)=1$ and $f_m(n)=0$ ; consequently $\lVert f_n-f_m\rVert_\infty\ge1$ .

givenalgebra

2.1

Every infinite subsequence contains two indices separated by at least $2$ , so no subsequence is uniformly Cauchy.

step 1.2algebra

3.1

By [L1], no subsequence can converge uniformly.

L1step 2.1algebra∎

Depends on

A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

The Ascoli--Arzelà Theorem (MIT) (standard reference, not scraped)

Translations of a fixed bump on R\mathbb RR are uniformly bounded and equicontinuous but have no uniformly convergent subsequence