PropositionStatement: AI-adaptedProof: AI-generatedSession-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.

Topological-domain equicontinuity agrees with metric equicontinuity on a metric domain

Statement

Let $(X, d_{X})$ and $(Y, d_{Y})$ be metric spaces, give $X$ its metric topology, and let $F \subseteq C (X, Y)$ . Then $F$ is equicontinuous in the topological-domain sense if and only if it is equicontinuous in the published metric epsilon-delta sense.

Facts & Assumptions

Given: Metric spaces $X, Y$ and a family $F \subseteq C (X, Y)$ .

[L1]

Topological-domain equicontinuity requires, for each $x$ and $ε > 0$ , one neighbourhood $U$ of $x$ on which every $f \in F$ satisfies $d_{Y} (f (y), f (x)) < ε$ (Equicontinuity on a topological domain and pointwise relative compactness).

[L2]

Metric equicontinuity requires, for each $x$ and $ε > 0$ , one $δ > 0$ such that $d_{X} (x, y) < δ$ implies $d_{Y} (f (x), f (y)) < ε$ for all $f \in F$ (Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces).

[L3]

Every metric neighbourhood of $x$ contains a positive-radius open ball about $x$ (The balls $B (x, 1 / n)$ , $n \geq 1$ , form a countable neighbourhood base at $x$ , so every metric space is first countable).

Proof

technique · direct

1.1

Suppose [L1] holds, and fix $x \in X$ and $ε > 0$ . Choose its common neighbourhood $U$ ; by [L3], some ball $B (x, δ)$ lies in $U$ . The same $δ$ works for every $f \in F$ , so [L2] holds.

L1L3

1.2

Conversely suppose [L2] holds. For fixed $x$ and $ε > 0$ , let $δ > 0$ be the common radius supplied there. The open neighbourhood $B (x, δ)$ then satisfies [L1] for every $f \in F$ .

L1L2

2.1

Steps 1.1 and 1.2 prove both directions without changing the order of the family quantifier.

step 1.1step 1.2∎

Depends on

Used by

Ascoli–Arzelà in the uniform topology for nonempty compact metric domains Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 84 results over 16 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, Section 45 (standard reference, not scraped)