Alphabeta Math
TheoremStatement: AI-adaptedProof: 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.

If X is a locally compact metric space then the evaluation map is continuous for the compact-open topology

Statement

Let (X,d) be a locally compact metric space (Locally compact metric space: every point has a compact neighbourhood) carrying its metric topology, let (Y,TY) be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), and give C(X,Y) 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}). Then the evaluation map

e:C(X,Y)×X→Y,e(f,x)=f(x)

(The evaluation map e:C(X,Y)×X→Y, e(f,x)=f(x)) is continuous, the product carrying the product topology (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

No hypothesis whatever is placed on Y, which is an arbitrary topological space: the argument uses only that a point of Y lies in an open set. No choice principle is used.

Local compactness is not removable. This page records as a false statement that the evaluation map is continuous for every metric domain, and its witness is X=Q, a metric space that is locally compact at no point.

Facts & Assumptions

Given: A locally compact metric space (X,d) with its metric topology, a topological space (Y,TY), the set C(X,Y) with the compact-open topology, and the evaluation map e.

[L1]

A map h into Y is continuous exactly when for every point p of its domain and every open V⊆Y with h(p)∈V there is an open U of the domain with p∈U and h[U]⊆V (Continuity of a map of topological spaces at a point and globally, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and f(A‾)⊆f(A)‾).

[L3]

S(K,V)={ g∈C(X,Y):g[K]⊆V } is open in the compact-open topology for every compact K⊆X and open V⊆Y (The compact-open topology on C(X,Y) for a metric domain X, with subbasis S(K,V)={f:f[K]⊆V}).

[L6]

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

Proof

technique · direct
1.1

Let (f,x)∈C(X,Y)×X and let V⊆Y be open with e(f,x)=f(x)∈V.

L1
1.2

Local compactness gives a real r0>0 such that Bˉ(x,r) is compact for every real r with 0<r<r0.

L4choose
2.1

f−1[V] is open in X and contains x, so there is a real s>0 with B(x,s)⊆f−1[V].

step 1.1L5L7choose
3.1

Put r:=min⁡{s,r0}/2, a real with 0<r, r<r0 and r<s; then K:=Bˉ(x,r) is compact and K⊆B(x,s)⊆f−1[V], that is f[K]⊆V.

step 2.1step 1.2L5L6
4.1

Hence f∈S(K,V), which is open in the compact-open topology, and x∈B(x,r), which is open in X; so S(K,V)×B(x,r) is an open subset of the product containing (f,x).

step 3.1L2L3L5
5.1

For every (g,y)∈S(K,V)×B(x,r): y∈B(x,r)⊆Bˉ(x,r)=K and g[K]⊆V, so e(g,y)=g(y)∈V; that is, e[S(K,V)×B(x,r)]⊆V.

step 3.1step 4.1L3L5
6.1

Steps 4.1 and 5.1 exhibit, for the arbitrary point (f,x) and the arbitrary open V containing its image, an open set of the product around (f,x) mapped into V; so e is continuous.

step 1.1step 4.1step 5.1L1∎

Remarks

  • What the compact-open topology is doing. The whole proof is the single observation that S(K,V) constrains a function on the whole of the compact set K, so once K is a neighbourhood of x the constraint survives moving the point as well as moving the function. A topology whose basic sets constrain a function at finitely many points only, such as the topology of pointwise convergence, cannot do this, and the evaluation map is in general not continuous for it.

  • Where local compactness is spent. Once, at step 1.2, to produce a compact neighbourhood of x inside the open set f−1[V]. Every metric space has arbitrarily small closed balls inside such an open set; what local compactness adds is that they may be taken compact.

  • The converse is not asserted. Nothing here says that continuity of the evaluation map forces X to be locally compact. That direction is true for Hausdorff spaces in the general theory and is not proved in this library.

Depends on

Used by

Dependency tree · two levels

60 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