Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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.

On C(R,R) the compact-open topology has the sets {g:sup⁡[−m,m]∣f−g∣<ε} as a neighbourhood base, and R is locally compact so evaluation is continuous

Example

Let R carry its usual metric d(s,t)=∣s−t∣ (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded) and let C(R,R) carry the compact-open topology (The compact-open topology on C(X,Y) for a metric domain X, with subbasis S(K,V)={f:f[K]⊆V}). For a natural m≥1 write [−m,m]:={ t∈R:−ι(m)≤t≤ι(m) } (Intervals of R: the nine order-convex forms, nondegeneracy, and length, The canonical natural ι(n)=n⋅1F of a field). Then:

  1. every [−m,m] is a compact subset of R, and every compact K⊆R is contained in some [−m,m];
  2. for each f∈C(R,R) the sets B[−m,m](f,ε)={ g∈C(R,R):∣f(t)−g(t)∣<ε for every t∈[−m,m] }(m≥1, ε>0) form a neighbourhood base at f in the compact-open topology (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open);
  3. R is a locally compact metric space (Locally compact metric space: every point has a compact neighbourhood), so the evaluation map e:C(R,R)×R→R is continuous (If X is a locally compact metric space then the evaluation map is continuous for the compact-open topology, The evaluation map e:C(X,Y)×X→Y, e(f,x)=f(x)).

The quantity sup⁡t∈[−m,m]∣f(t)−g(t)∣ of the title exists and is a maximum, by fact (U3) of The topology of compact convergence on C(X,Y) for metric X and Y: uniform convergence on each compact subset of X; the formulation in claim 2 avoids writing it, which is what keeps the empty compact set harmless elsewhere on this page.

Facts & Assumptions

Given: R with the usual metric, C(R,R) with the compact-open topology, and for a natural m≥1 the interval [−m,m].

[L3]

For every real x there is a natural m≥1 with x<ι(m), and ι is strictly increasing with ι(m)>0 for m≥1 (Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing, The canonical natural ι(n)=n⋅1F of a field).

[L5]

If K⊆K′ are compact then BK′(f,ε)⊆BK(f,ε), the defining condition on K′ being stronger (The topology of compact convergence on C(X,Y) for metric X and Y: uniform convergence on each compact subset of X).

[L7]

The maximum of a two-element set of reals exists and is one of them (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Verification

technique · direct
1.1

[−m,m] is bounded, lying in B(0,ι(m)+1), and closed in R, since a point y with y>ι(m) has B(y,y−ι(m)) inside the complement and a point with y<−ι(m) has B(y,−ι(m)−y) inside it; so [−m,m] is a compact subset of R.

L1L2
2.1

Let K⊆R be compact; it is bounded, so fix a real r>0 with ∣t∣<r for every t∈K, and then a natural m≥1 with r<ι(m); every t∈K satisfies −ι(m)≤t≤ι(m), that is K⊆[−m,m]. This with step 1.1 is claim 1.

step 1.1L1L3choose
2.2

For claim 3, let x∈R and take a natural m≥1 with ∣x∣+1<ι(m); then [−m,m] is compact by step 1.1 and B(x,1)⊆[−m,m], since ∣t−x∣<1 gives ∣t∣≤∣x∣+1<ι(m) by the triangle inequality for the absolute value.

step 1.1L3L7choose
3.1

For claim 2, fix f∈C(R,R) and let N be a neighbourhood of f in the compact-open topology; since that topology is the topology of compact convergence, there are a compact K and a real ε>0 with BK(f,ε)⊆N.

step 2.1L4choose
4.1

Take m≥1 with K⊆[−m,m]; then B[−m,m](f,ε)⊆BK(f,ε)⊆N, and f∈B[−m,m](f,ε), which is itself a neighbourhood of f by step 1.1 and [L4]; so the displayed family is a neighbourhood base at f, which is claim 2.

step 1.1step 2.1step 3.1L4L5
5.1

So every point of R has a compact set containing a ball around it, that is R is a locally compact metric space; hence the evaluation map on C(R,R) is continuous, which is claim 3.

step 2.2L6∎

Remarks

  • Claim 2 is what makes the compact-open topology on C(R,R) concrete. A general neighbourhood in it involves an arbitrary compact set and an arbitrary open subset of the target; claim 2 replaces both by a bound on a symmetric interval and a single ε, and the intervals may be indexed by the naturals. That is the shape a metrization proof would exploit, and this library does not carry out that proof.

  • Local compactness of R is where Heine-Borel is spent. In a general metric space a closed ball need not be compact, and then nothing above survives; what makes R work is that closed bounded sets are compact (Heine-Borel in Rn: with the Euclidean metric a subset of Rn 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). The contrast is Q, where the evaluation map is not continuous at all.

  • The intervals [−m,m] exhaust R, and that is claim 1's real content. Every compact subset sits inside one of countably many of them, so the compact sets, of which there are very many, are controlled by a countable family. Nothing about metrizability follows from this alone, and none is claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

89 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