LemmaStatement: 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.

The pointwise closure of an equicontinuous family is equicontinuous and consists of continuous maps

Statement

Let $X$ be a topological space, let $Y$ be a metric space, and let $F \subseteq C (X, Y)$ be equicontinuous. The closure $H$ of $F$ in $Y^{X}$ with the topology of pointwise convergence is equicontinuous, and every $h \in H$ is continuous.

Facts & Assumptions

Given: A topological space $X$ , a metric space $Y$ , and an equicontinuous family $F \subseteq C (X, Y)$ with pointwise closure $H$ .

[L1]

Equicontinuity supplies, for fixed $x$ and tolerance, one neighbourhood of $x$ that works for every member of the family (Equicontinuity on a topological domain and pointwise relative compactness).

[L2]

A basic pointwise neighbourhood controls finitely many coordinate values (The topology of pointwise convergence on $Y^{X}$ , which is the product topology, and its restriction to $C (X, Y)$ ).

[L3]

Coordinate inverse images of open sets are subbasic open in a 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).

Proof

technique · direct

1.1

Fix $x \in X$ and $ε > 0$ . By [L1], choose a neighbourhood $U$ of $x$ such that $d (f (y), f (x)) < ε / 3$ for every $f \in F$ and $y \in U$ .

1.2

Fix $h \in H$ and $y \in U$ . The pointwise neighbourhood of $h$ requiring both $d (g (x), h (x)) < ε / 3$ and $d (g (y), h (y)) < ε / 3$ meets $F$ ; choose $f$ in the intersection.

L2L3

2.1

The triangle inequality and steps 1.1--1.2 give $d (h (y), h (x)) < ε$ . The neighbourhood $U$ did not depend on $h$ , so it proves equicontinuity of all of $H$ .

step 1.1step 1.2

3.1

For each fixed $h \in H$ , the estimate in step 2.1 is the neighbourhood criterion for continuity at every $x$ . Hence every member of $H$ is continuous.

step 2.1∎

Depends on

Used by

Under Choice, equicontinuity and pointwise relative compactness give compact compact-open closure Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 40 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.3 (standard reference, not scraped)