Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge 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.

The evaluation map e:C(X,Y)×XYe : C(X,Y) \times X \to Y, e(f,x)=f(x)e(f,x) = f(x)

Definition

Let (X,d)(X,d) be a metric space carrying its metric topology (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not), let (Y,TY)(Y,\mathcal{T}_Y) be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), and let C(X,Y)C(X,Y) carry the compact-open topology (The compact-open topology on C(X,Y)C(X,Y) for a metric domain XX, with subbasis S(K,V)={f:f[K]V}S(K,V) = \{f : f[K] \subseteq V\}). The evaluation map is

e:C(X,Y)×XY,e(f,x):=f(x),e : C(X,Y) \times X \longrightarrow Y, \qquad e(f,x) := f(x),

the domain carrying the product topology (The product set iIXi\prod_{i \in I} X_i 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) of the compact-open topology on C(X,Y)C(X,Y) and the metric topology on XX.

This is a function. For fC(X,Y)f \in C(X,Y) and xXx \in X the value f(x)f(x) is a well-determined element of YY, and a pair (f,x)(f,x) of the product determines both entries (The product set iIXi\prod_{i \in I} X_i 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), so ee is defined on all of C(X,Y)×XC(X,Y) \times X with no further condition.

Which topology is meant is part of the definition. Continuity of ee is a statement about the pair of topologies on the source and the topology on the target (Continuity of a map of topological spaces at a point and globally), and C(X,Y)C(X,Y) carries several topologies on this page. Unless another is named, the topology on C(X,Y)C(X,Y) inside an evaluation map is the compact-open one; where a subspace of C(X,Y)C(X,Y) is evaluated, it carries the subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

Separate continuity is immediate; joint continuity is not. For fixed fC(X,Y)f \in C(X,Y) the map xe(f,x)=f(x)x \mapsto e(f,x) = f(x) is continuous, being ff itself. For fixed xXx \in X the map fe(f,x)=f(x)f \mapsto e(f,x) = f(x) is continuous as well, since for open VYV \subseteq Y its preimage is S({x},V)S(\{x\},V), a subbasic open set of the compact-open topology, {x}\{x\} being compact (The compact-open topology on C(X,Y)C(X,Y) for a metric domain XX, with subbasis S(K,V)={f:f[K]V}S(K,V) = \{f : f[K] \subseteq V\}). What is at issue on this page is joint continuity, that is continuity of ee on the product, and that genuinely needs a hypothesis on XX: it holds when XX is locally compact, and this page records as a false statement that it holds for every metric XX, with an explicit witness.

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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