TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

A uniform limit of continuous functions is continuous, so $C (X, Y)$ is closed in $Y^{X}$ under the uniform metric

Statement

Let $(X, T_{X})$ be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and let $(Y, d)$ be a metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) carrying its metric topology. Then:

The $ε / 3$ criterion. Let $f : X \to Y$ be a function such that for every real $ε > 0$ there is a continuous $g : X \to Y$ with $d (f (x), g (x)) < ε for every x \in X .$ Then $f$ is continuous (Continuity of a map of topological spaces at a point and globally).
Uniform limit theorem. If $X$ is nonempty, $(f_{k})$ is a sequence of continuous maps $X \to Y$ and $(f_{k})$ converges uniformly to $f$ (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ ), then $f$ is continuous.
Closedness. If $X$ is nonempty, $C (X, Y)$ is a closed subset of $(Y^{X}, \overset{ˉ}{ρ})$ , the uniform metric being that of For a nonempty set $X$ and a metric space $(Y, d)$ the uniform metric $\overset{ˉ}{ρ} (f, g) = \sup_{x} \min {d (f (x), g (x)), 1}$ is a metric on $Y^{X}$ .

The domain is an arbitrary topological space, not a metric space: nothing in the argument uses a distance in $X$ . Only the target carries a metric, and it carries one because the hypothesis of claim 1 is a statement about distances in $Y$ .

No choice principle is used, and claim 3 in particular is choice free. The proof of claim 3 instantiates one continuous $g$ for each $ε$ and uses it immediately, rather than manufacturing a sequence of them; a sequential argument through A point lies in the closure of $A$ iff some sequence in $A$ converges to it, and a set is closed iff it is sequentially closed would spend the Axiom of Countable Choice, and that route is deliberately not taken.

Facts & Assumptions

Given: A topological space $(X, T_{X})$ , a metric space $(Y, d)$ with its metric topology, and where claims 2 and 3 apply, a nonempty $X$ and the uniform metric $\overset{ˉ}{ρ}$ on $Y^{X}$ with $\overset{ˉ}{d} = \min {d, 1}$ .

[L1]

$h : X \to Y$ is continuous at $a$ exactly when for every open $V \subseteq Y$ with $h (a) \in V$ there is an open $U \subseteq X$ with $a \in U$ and $h [U] \subseteq V$ ; and $h$ is continuous exactly when it is continuous at every point (Continuity of a map of topological spaces at a point and globally, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

[L2]

In a metric space the balls $B (p, ε)$ , $ε > 0$ , are open and form a neighbourhood base at $p$ : an open $V$ with $p \in V$ contains some $B (p, ε)$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space, The balls $B (x, 1 / n)$ , $n \geq 1$ , form a countable neighbourhood base at $x$ , so every metric space is first countable, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

[L3]

The triangle inequality (M3) and symmetry (M2) of $d$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L4]

Uniform convergence of $(f_{k})$ to $f$ gives, for each real $ε > 0$ , an index $K$ with $d (f_{k} (x), f (x)) < ε$ for every $x \in X$ and every $k \geq K$ (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ , Convergence in the uniform metric is exactly uniform convergence: one $N$ serving every point).

[L5]

For nonempty $A \subseteq Y^{X}$ the closure in $(Y^{X}, \overset{ˉ}{ρ})$ is $\overline{A} = {u : \overset{ˉ}{ρ} (u, A) = 0}$ , a set is closed exactly when it equals its closure, and $\emptyset$ is closed (The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[L6]

If $\inf S = 0$ and $η > 0$ is real, then some $s \in S$ satisfies $s < η$ (Epsilon characterisation of the infimum, Greatest lower bound (infimum)).

[L7]

$\overset{ˉ}{d} \leq d$ and $\overset{ˉ}{d} \leq 1$ ; if $\overset{ˉ}{d} (u, v) < 1$ then $\overset{ˉ}{d} (u, v) = d (u, v)$ ; and $\overset{ˉ}{d} (u (x), v (x)) \leq \overset{ˉ}{ρ} (u, v)$ for every $x \in X$ ( $\min (d, 1)$ and $d / (1 + d)$ are metrics uniformly equivalent to $d$ , so every metric space carries a bounded metric with the same topology, For a nonempty set $X$ and a metric space $(Y, d)$ the uniform metric $\overset{ˉ}{ρ} (f, g) = \sup_{x} \min {d (f (x), g (x)), 1}$ is a metric on $Y^{X}$ , Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L8]

Two elements of $Y^{X}$ are equal exactly when they agree at every point of $X$ , and $Y^{X}$ is the set of all functions $X \to Y$ (The topology of pointwise convergence on $Y^{X}$ , which is the product topology, and its restriction to $C (X, Y)$ ).

Proof

technique · direct

1.1

For claim 1, assume the displayed hypothesis, fix $a \in X$ , and let $V \subseteq Y$ be open with $f (a) \in V$ ; fix a real $ε > 0$ with $B (f (a), ε) \subseteq V$ .

assume-hypL1L2choose

1.2

For claim 3, if $C (X, Y) = \emptyset$ then it is closed and there is nothing to prove; so assume $C (X, Y) \neq \emptyset$ and let $f$ lie in the closure of $C (X, Y)$ in $(Y^{X}, \overset{ˉ}{ρ})$ , so that $\overset{ˉ}{ρ} (f, C (X, Y)) = 0$ .

L5assume-hyp

2.1

Apply the hypothesis at $ε / 3$ : fix a continuous $g : X \to Y$ with $d (f (x), g (x)) < ε / 3$ for every $x \in X$ .

step 1.1choose

2.2

Let $ε_{1} > 0$ be real and put $η : = \min {ε_{1}, 1} / 2$ , a real with $0 < η \leq 1 / 2 < 1$ and $η < ε_{1}$ ; since the infimum of the distances from $f$ to the members of $C (X, Y)$ is $0 < η$ , there is $g \in C (X, Y)$ with $\overset{ˉ}{ρ} (f, g) < η$ .

step 1.2L6L7choose

3.1

$B (g (a), ε / 3)$ is open in $Y$ and contains $g (a)$ , so continuity of $g$ at $a$ gives an open $U \subseteq X$ with $a \in U$ and $g [U] \subseteq B (g (a), ε / 3)$ .

step 2.1L1L2choose

3.2

For every $x \in X$ : $\overset{ˉ}{d} (f (x), g (x)) \leq \overset{ˉ}{ρ} (f, g) < η < 1$ , hence $d (f (x), g (x)) = \overset{ˉ}{d} (f (x), g (x)) < η < ε_{1}$ .

step 2.2L7

4.1

For every $x \in U$ : $d (f (x), f (a)) \leq d (f (x), g (x)) + d (g (x), g (a)) + d (g (a), f (a)) < ε / 3 + ε / 3 + ε / 3 = ε$ , so $f [U] \subseteq B (f (a), ε) \subseteq V$ .

step 1.1step 2.1step 3.1L3

5.1

As $V$ was an arbitrary open set containing $f (a)$ and $a$ an arbitrary point of $X$ , step 4.1 makes $f$ continuous at every point, hence continuous; this is claim 1.

step 1.1step 4.1L1

6.1

For claim 2, let $ε > 0$ be real; uniform convergence gives an index $K$ with $d (f_{k} (x), f (x)) < ε$ for every $x \in X$ and every $k \geq K$ , so the continuous map $g : = f_{K}$ witnesses the hypothesis of claim 1 at $ε$ ; hence $f$ is continuous by claim 1.

step 5.1L4

6.2

Steps 2.2 and 3.2 supply, for each real $ε_{1} > 0$ , a continuous $g$ with $d (f (x), g (x)) < ε_{1}$ for every $x \in X$ , which is the hypothesis of claim 1; so $f$ is continuous, that is $f \in C (X, Y)$ .

step 5.1step 2.2step 3.2L8

7.1

Hence the closure of $C (X, Y)$ is contained in $C (X, Y)$ , and containing it always, it equals it; so $C (X, Y)$ is closed in $(Y^{X}, \overset{ˉ}{ρ})$ , which is claim 3.

step 1.2step 6.2L5∎

Remarks

The three thirds are the three legs of the estimate, and each is a different approximation: $f$ to $g$ at $x$ , $g$ at $x$ to $g$ at $a$ , and $g$ to $f$ at $a$ . Only the middle one uses continuity, and only the outer two use that the approximation of $f$ by $g$ is uniform. If the approximation were merely pointwise, the third leg would still hold but the first would need an $ε$ depending on $x$ , and the argument collapses; the companion page exhibits exactly that collapse.
Claim 3 is what makes $C (X, Y)$ a complete space when $Y$ is complete, by the next item, and it is the reason the uniform topology and not the pointwise one is the natural home for limits of continuous functions. In the pointwise topology $C (X, Y)$ is in general not closed, and the companion page carries a witness on $[0, 1]$ .
Why the choice-free route was taken. The usual proof of claim 3 shows that $C (X, Y)$ is sequentially closed and then invokes A point lies in the closure of $A$ iff some sequence in $A$ converges to it, and a set is closed iff it is sequentially closed to conclude closedness; that item's forward direction spends the Axiom of Countable Choice, since it manufactures a sequence out of adherence. The argument above instead works with the distance to the set directly and instantiates a single $g$ at each $ε$ , so claim 3 is a theorem of ZF.

Depends on

Used by

Dependency tree · two levels

78 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

Uniform limit theorem (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §21 (standard reference, not scraped)

A uniform limit of continuous functions is continuous, so C(X,Y)C(X,Y) is closed in YXYX under the uniform metric