ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

Translated tent functions on $R$ converge to zero in the compact-open topology

Example

For $k \in N$ , define

$f_{k} (x) : = \max {1 - ∣ x - k ∣, 0} (x \in R) .$

Then each $f_{k}$ is continuous and $1$ -Lipschitz, and $f_{k} \to 0$ in the compact-open topology on $C (R, R)$ , but the sequence does not converge uniformly on $R$ .

Facts & Assumptions

Given: The translated tent functions $(f_{k})$ on the real line.

[L1]

The general and published metric-domain compact-open topologies agree (The general compact-open topology agrees with the published metric-domain definition).

[L2]

For metric domain and target, compact-open convergence is compact convergence (For a metric domain and a metric target the compact-open topology on $C (X, Y)$ is the topology of compact convergence).

[L3]

Every compact subset of $R$ is bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L4]

The Archimedean property provides a natural number larger than any prescribed real (Every complete ordered field is Archimedean).

[L5]

Uniform convergence requires one tail index to work at every point of the domain (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ ).

[L6]

General compact-open subbasic conditions test images of compact sets (The compact-open topology on $C (X, Y)$ for arbitrary topological spaces).

Verification

technique · direct

1.1

The map $x \mapsto 1 - ∣ x - k ∣$ is $1$ -Lipschitz, and taking the maximum with $0$ preserves that bound. Hence every $f_{k}$ is continuous and $1$ -Lipschitz.

algebra

1.2

Let $K \subseteq R$ be compact. If $K = \emptyset$ , convergence on $K$ is vacuous. Otherwise [L3] gives $R > 0$ with $∣ x ∣ \leq R$ for $x \in K$ , and [L4] gives $N \in N$ with $N > R + 1$ .

L3L4

2.1

If $k \geq N$ and $x \in K$ , then $∣ x - k ∣ \geq k - ∣ x ∣ > 1$ , so $f_{k} (x) = 0$ . Thus the sequence is eventually identically zero on every compact $K$ , and therefore converges to zero uniformly on each compact set.

step 1.2

3.1

By [L1], [L2], and [L6], step 2.1 is convergence in the general compact-open topology.

L1L2L6step 2.1

4.1

Yet $f_{k} (k) = 1$ for every $k$ , so no tail has $∣ f_{k} (x) ∣ < 1 / 2$ for every $x \in R$ . By [L5], convergence is not uniform on the whole real line.

L5∎

Depends on

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: 129 results over 20 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, BBT (standard reference, not scraped)

Translated tent functions on RR converge to zero in the compact-open topology