TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Evaluation is continuous for the compact-open topology on a locally compact Hausdorff domain

Statement

Let $X$ be a locally compact Hausdorff space and let $Y$ be a topological space. Give $C (X, Y)$ the compact-open topology. Then the evaluation map

$ev : C (X, Y) \times X ⟶ Y, ev (f, x) = f (x),$

is continuous. The assertion includes the empty domain, where the product domain is empty.

Facts & Assumptions

Given: A locally compact Hausdorff space $X$ and a topological space $Y$ .

[L1]

A compact-open subbasic neighbourhood has the form $S (K, W) = {g : g [K] \subseteq W}$ for compact $K \subseteq X$ and open $W \subseteq Y$ (The compact-open topology on $C (X, Y)$ for arbitrary topological spaces).

[L2]

If $X$ is locally compact Hausdorff, $x \in O$ , and $O$ is open, then some open $U$ satisfies $x \in U \subseteq \overline{U} \subseteq O$ with $\overline{U}$ compact (In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure).

[L3]

Products of open sets form a basis for 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).

[L4]

A continuous map pulls an open set back to an open set (Continuity of a map of topological spaces at a point and globally).

Proof

technique · direct

1.1

If $X = \emptyset$ , the domain $C (X, Y) \times X$ is empty, so evaluation is continuous. Assume henceforth that $(f, x) \in C (X, Y) \times X$ and that $W \subseteq Y$ is open with $f (x) \in W$ .

1.2

By [L4], $O = f^{- 1} [W]$ is open and contains $x$ . By [L2], choose open $U$ with $x \in U \subseteq K : = \overline{U} \subseteq O$ and $K$ compact.

L2L4

2.1

The set $S (K, W) \times U$ is an open product neighbourhood of $(f, x)$ : $f [K] \subseteq W$ , $S (K, W)$ is subbasic open, and [L3] applies.

L1L3step 1.2

3.1

If $(g, y) \in S (K, W) \times U$ , then $y \in U \subseteq K$ and $g (y) \in W$ . Thus evaluation maps this neighbourhood into $W$ , proving continuity.

step 2.1∎

Depends on

Used by

A compact compact-open family is equicontinuous on a locally compact Hausdorff domain Theorem

Dependency tree · next 3 levels

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

Topology, second edition, Theorem 46.10 (standard reference, not scraped)