LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The compact-open and pointwise topologies agree on an equicontinuous family

Statement

Let $X$ be a topological space, let $Y$ be a metric space, and let $E \subseteq C (X, Y)$ be equicontinuous. The compact-open and pointwise subspace topologies on $E$ are equal.

Facts & Assumptions

Given: A topological space $X$ , a metric space $Y$ , and an equicontinuous family $E \subseteq C (X, Y)$ .

[L1]

Compact-open subbasic sets are $S (K, V) = {g : g [K] \subseteq V}$ for compact $K$ and open $V$ (The compact-open topology on $C (X, Y)$ for arbitrary topological spaces).

[L2]

Equicontinuity at a point gives one neighbourhood on which all members of the family have a prescribed variation (Equicontinuity on a topological domain and pointwise relative compactness).

[L3]

Pointwise basic neighbourhoods prescribe values at finitely many points (The topology of pointwise convergence on $Y^{X}$ , which is the product topology, and its restriction to $C (X, Y)$ ).

[L4]

A subset is compact intrinsically exactly when it is compact as a subspace of an ambient topological space (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).

Proof

technique · direct

1.1L1L3L4

For $x \in X$ and open $V \subseteq Y$ , the pointwise subbasic set ${g : g (x) \in V}$ is $S ({x}, V)$ ; the singleton is compact. Thus the compact-open topology on $E$ is finer than the pointwise topology.

1.2L1L2

Fix $f \in E \cap S (K, V)$ . If $K = \emptyset$ or $V = Y$ , the whole family is a pointwise neighbourhood contained in $S (K, V)$ . Otherwise, let $I$ be the set of triples $(x, r, U)$ with $x \in K$ , $r > 0$ , $U$ an open neighbourhood of $x$ , $B (f (x), 3 r) \subseteq V$ , $d (f (y), f (x)) < r$ on $U$ , and $d (g (y), g (x)) < r$ on $U$ for all $g \in E$ .

1.3L2

Openness of $V$ , continuity of $f$ , and [L2] show that every $x \in K$ occurs in some triple of $I$ . Hence the open sets $U$ from all triples in $I$ cover $K$ , without choosing one triple for every point.

2.1L3L4step 1.3

Compactness of $K$ supplies finitely many triples $(x_{i}, r_{i}, U_{i})$ from $I$ with $K \subseteq U_{1} \cup \dots \cup U_{m}$ . Let $N$ be the pointwise neighbourhood of $f$ in $E$ defined by $d (g (x_{i}), f (x_{i})) < r_{i}$ for every $i$ .

3.1step 1.2step 2.1

If $g \in N$ and $y \in K$ , choose $i$ with $y \in U_{i}$ . The three inequalities attached to $(x_{i}, r_{i}, U_{i})$ and the definition of $N$ give $d (g (y), f (x_{i})) < 3 r_{i}$ , so $g (y) \in V$ . Hence $N \subseteq S (K, V)$ .

4.1step 1.1step 3.1∎

Every compact-open subbasic neighbourhood has a pointwise neighbourhood inside it, so the pointwise topology on $E$ is finer. Step 1.1 proves equality.

Depends on

Used by

Dependency tree · two levels

16 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

Topology, second edition, Lemma 47.2 (standard reference, not scraped)