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

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.

L1L3L4

1.2

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$ .

L1L2

1.3

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.1

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$ .

L3L4step 1.3

3.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)$ .

step 1.2step 2.1

4.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.

step 1.1step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 33 results over 10 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, Lemma 47.2 (standard reference, not scraped)