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

Translations of a fixed bump on $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 $ε$ -- $δ$ 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 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 $ε > 0$ , the common choice $δ = ε$ gives $∣ x - y ∣ < δ \Rightarrow ∣ f_{n} (x) - f_{n} (y) ∣ < ε$ for every $n$ ; this is the ordinary all-metric-space equicontinuity condition used in the refuted claim.

givenalgebra

1.2

If $∣ m - n ∣ \geq 2$ , then at $x = n$ one has $f_{n} (n) = 1$ and $f_{m} (n) = 0$ ; consequently $∥ f_{n} - f_{m} ∥_{\infty} \geq 1$ .

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 · two levels

4 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

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

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