TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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 $f : X \times Z \to Y$ is continuous then its transpose $F : Z \to C(X,Y)$ , $F(z)(x) = f(x,z)$ , is continuous for the compact-open topology, with no hypothesis on $X$ beyond being metric

Statement

Let $(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 $Z$ and $Y$ be topological spaces (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), and let

$f : X \times Z \to Y$

be continuous, the product carrying the product topology (The product set $\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). For $z \in Z$ define $F(z) : X \to Y$ by $F(z)(x) := f(x,z)$ . Then:

$F(z) \in C(X,Y)$ for every $z \in Z$ ;
the transpose $F : Z \to C(X,Y)$ is continuous when $C(X,Y)$ carries 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] \subseteq V\}$ ).

No local compactness and no separation hypothesis is used, on any of the three spaces; $X$ is metric only because the compact-open topology is defined here over the compact subsets of a metric space. No choice principle is used.

Facts & Assumptions

Given: A metric space $(X,d)$ with its metric topology, topological spaces $Z$ and $Y$ , a continuous $f : X \times Z \to Y$ , and $F(z)(x) = f(x,z)$ .

[L1]

A map $h$ into a product is continuous exactly when each of its components is, the components being the composites with the projections; the projections are continuous (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice, claims 1 and 2, The product set $\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).

[L2]

A composite of continuous maps is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 1).

[L3]

A constant map into a topological space is continuous, the preimage of an open set being the whole domain or the empty set, both open (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(\overline{A}) \subseteq \overline{f(A)}$ , clause (b), Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L4]

The identity map of a topological space is continuous, being its own preimage assignment (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(\overline{A}) \subseteq \overline{f(A)}$ , clause (b)).

[L5]

Continuity may be checked on a subbasis: $h$ is continuous exactly when $h^{-1}[S]$ is open for every member $S$ of a subbasis of the target (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(\overline{A}) \subseteq \overline{f(A)}$ , clause (d), Basis and subbasis for a topology, and the topology generated by a family of sets, A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis).

[L6]

The sets $S(K,V) = \{\, g \in C(X,Y) : g[K] \subseteq V \,\}$ , for compact $K \subseteq X$ and open $V \subseteq Y$ , are a subbasis for the compact-open topology on $C(X,Y)$ (The compact-open topology on $C(X,Y)$ for a metric domain $X$ , with subbasis $S(K,V) = \{f : f[K] \subseteq V\}$ , Open cover, subcover, compact metric space, and compact subset of a metric space, A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).

[L7]

Tube lemma: for compact $K \subseteq X$ , a point $z_0 \in Z$ and an open $N \subseteq X \times Z$ with $K \times \{z_0\} \subseteq N$ there is an open $W \subseteq Z$ with $z_0 \in W$ and $K \times W \subseteq N$ (Tube lemma: if $K$ is a compact subset of a metric space $X$ , $Z$ is a topological space and $N$ is open in $X \times Z$ with $K \times \{z_0\} \subseteq N$ , then $K \times W \subseteq N$ for some open $W \ni z_0$ ).

[L8]

A subset of a topological space is open exactly when it is a neighbourhood of each of its points, that is when each of its points lies in an open set inside it (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, consequence 4).

[L9]

$f$ is continuous, so $f^{-1}[V]$ is open in $X \times Z$ for every open $V \subseteq Y$ (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(\overline{A}) \subseteq \overline{f(A)}$ , clause (b)).

Proof

technique · direct

1.1

Fix $z \in Z$ and let $j_z : X \to X \times Z$ be the map $j_z(x) := (x,z)$ ; its components are the identity of $X$ and the constant map at $z$ , both continuous, so $j_z$ is continuous.

L1L3L4

2.1

$F(z) = f \circ j_z$ , since $(f \circ j_z)(x) = f(x,z) = F(z)(x)$ for every $x \in X$ ; hence $F(z)$ is continuous and $F(z) \in C(X,Y)$ , which is claim 1.

step 1.1L2

3.1

For claim 2 it suffices, by [L5] and [L6], to show that $F^{-1}[S(K,V)]$ is open in $Z$ for every compact $K \subseteq X$ and every open $V \subseteq Y$ .

step 2.1L5L6suffices: preimages of subbasic sets are open

3.2

Unwinding the definitions, $F^{-1}[S(K,V)] = \{\, z \in Z : F(z)[K] \subseteq V \,\} = \{\, z \in Z : f(x,z) \in V \text{ for every } x \in K \,\}$ .

step 2.1L6

4.1

Let $z_0 \in F^{-1}[S(K,V)]$ and put $N := f^{-1}[V]$ , an open subset of $X \times Z$ ; by step 3.2 every $x \in K$ satisfies $f(x,z_0) \in V$ , that is $K \times \{z_0\} \subseteq N$ .

step 3.2L9

5.1

The tube lemma applied to $K$ , $z_0$ and $N$ gives an open $W \subseteq Z$ with $z_0 \in W$ and $K \times W \subseteq N$ .

step 4.1L7choose

6.1

Every $z \in W$ then satisfies $f(x,z) \in V$ for every $x \in K$ , that is $z \in F^{-1}[S(K,V)]$ ; so $W$ is an open set with $z_0 \in W \subseteq F^{-1}[S(K,V)]$ .

step 3.2step 4.1step 5.1

7.1

As $z_0$ was an arbitrary point of $F^{-1}[S(K,V)]$ , that set is open in $Z$ ; by step 3.1 this proves claim 2.

step 3.1step 6.1L8∎

Remarks

The tube lemma is the entire content. The condition defining $F^{-1}[S(K,V)]$ is "the whole slice $K \times \{z\}$ lands in $V$ ", and openness of that condition in $z$ is exactly the statement that a neighbourhood of a slice contains a tube. Everything else is unwinding.
This half of the exponential law is the cheap half. It needs no hypothesis on $X$ beyond compactness being available for its subsets, and none at all on $Z$ or $Y$ . The converse half — that every continuous $F : Z \to C(X,Y)$ arises from a continuous $f$ — runs through continuity of the evaluation map and is where local compactness of $X$ is spent.
The map $F$ determines $f$ and conversely, as functions. That the assignment $f \mapsto F$ is injective, and that under the local compactness hypothesis it is onto the continuous maps $Z \to C(X,Y)$ , is the exponential law below; this theorem is the statement that the assignment lands in the right place.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 104 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

Compact-open topology (Wikipedia) (standard reference, not scraped)
Exponential law (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §46 (standard reference, not scraped)

If f:X×Z→Yf : X \times Z \to Yf:X×Z→Y is continuous then its transpose F:Z→C(X,Y)F : Z \to C(X,Y)F:Z→C(X,Y), F(z)(x)=f(x,z)F(z)(x) = f(x,z)F(z)(x)=f(x,z), is continuous for the compact-open topology, with no hypothesis on XXX beyond being metric