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

If $(Y,d)$ is complete then $Y^{X}$ is complete in the uniform metric, and so is $C(X,Y)$

Statement

Let $X$ be a nonempty set, let $(Y,d)$ be a complete metric space (Complete metric space: every Cauchy sequence converges in the space) and let $\bar\rho$ be the uniform metric on $Y^{X}$ (For a nonempty set $X$ and a metric space $(Y,d)$ the uniform metric $\bar\rho(f,g) = \sup_{x} \min\{d(f(x),g(x)), 1\}$ is a metric on $Y^{X}$ ). Then:

$(Y^{X}, \bar\rho)$ is a complete metric space.
If in addition $X$ carries a topology, then $C(X,Y)$ with the restriction of $\bar\rho$ (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C(X,Y)$ ) is a complete metric space.

No choice principle is used. The limit function is defined by a formula, not chosen: a Cauchy sequence in a complete metric space has exactly one limit (A sequence in a metric space has at most one limit), so $x \mapsto \lim_k f_k(x)$ is a function, and nothing is selected.

Facts & Assumptions

Given: A nonempty set $X$ , a complete metric space $(Y,d)$ , the truncated metric $\bar d = \min\{d,1\}$ on $Y$ , the uniform metric $\bar\rho$ on $Y^{X}$ , and a $\bar\rho$ -Cauchy sequence $(f_k)$ in $Y^{X}$ .

[L1]

$\bar d \le d$ and $\bar d \le 1$ ; if $\bar d(u,v) < 1$ then $\bar d(u,v) = d(u,v)$ ; and $\bar d(u(x),v(x)) \le \bar\rho(u,v)$ for every $x \in X$ , while any real bounding all the values $\bar d(u(x),v(x))$ above bounds $\bar\rho(u,v)$ ( $\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 $\bar\rho(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, Complete ordered field (least-upper-bound property), Suprema and infima are unique).

[L2]

$(x_k)$ is Cauchy in a metric space when for every real $\varepsilon > 0$ there is $K$ with the distance between $x_m$ and $x_n$ below $\varepsilon$ for all $m, n \ge K$ ; the rational and real tests agree (Cauchy sequence in a metric space, The rationals embed densely in the reals).

[L3]

Completeness of $(Y,d)$ : every $d$ -Cauchy sequence in $Y$ converges in $(Y,d)$ , and its limit is unique (Complete metric space: every Cauchy sequence converges in the space, A sequence in a metric space has at most one limit, Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$ ).

[L4]

$x_k \to p$ in a metric space means: for every real $\varepsilon > 0$ there is $K$ with the distance from $x_k$ to $p$ below $\varepsilon$ for every $k \ge K$ (Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$ , Open ball, closed ball and sphere in a metric space, The rationals embed densely in the reals).

[L5]

The triangle inequality (M3) for $\bar d$ ( $\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, Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L6]

$C(X,Y)$ is a closed subset of $(Y^{X},\bar\rho)$ when $X$ is a nonempty topological space (A uniform limit of continuous functions is continuous, so $C(X,Y)$ is closed in $Y^{X}$ under the uniform metric, claim 3).

[L7]

A closed subset of a complete metric space is complete in the subspace metric (A subspace of a complete metric space is complete iff it is closed, and a complete subspace of any metric space is closed, claim 2, Isometry, isometric embedding, and the subspace metric on a subset).

[L8]

Two elements of $Y^{X}$ are equal exactly when they agree at every point (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

Let $x \in X$ and let $\varepsilon > 0$ be real; put $\eta := \min\{\varepsilon, 1\}/2$ , a real with $0 < \eta \le 1/2 < 1$ and $\eta < \varepsilon$ , and take $K$ with $\bar\rho(f_m,f_n) < \eta$ for all $m,n \ge K$ .

givenL1L2choose

1.2

Let $\varepsilon > 0$ be real; put $\eta := \min\{\varepsilon,1\}/4$ , a real with $0 < \eta \le 1/4 < 1$ and $4\eta \le \varepsilon$ , and take $K$ with $\bar\rho(f_m,f_n) < \eta$ for all $m,n \ge K$ .

givenL1L2choose

2.1

For $m, n \ge K$ : $\bar d(f_m(x),f_n(x)) \le \bar\rho(f_m,f_n) < \eta < 1$ , hence $d(f_m(x),f_n(x)) = \bar d(f_m(x),f_n(x)) < \eta < \varepsilon$ .

step 1.1L1

3.1

As $\varepsilon$ was an arbitrary positive real, step 2.1 makes $(f_k(x))$ a $d$ -Cauchy sequence in $Y$ for every $x \in X$ ; by completeness it converges, and its limit is unique, so $f(x) := \lim_k f_k(x)$ defines a function $f \in Y^{X}$ with no selection made.

step 2.1L2L3L8

4.1

Fix $n \ge K$ and $x \in X$ ; since $f_m(x) \to f(x)$ in $(Y,d)$ and $\bar d \le d$ , there is $m \ge K$ with $\bar d(f_m(x), f(x)) < \eta$ , and then $\bar d(f_n(x), f(x)) \le \bar d(f_n(x), f_m(x)) + \bar d(f_m(x), f(x)) < \eta + \eta = 2\eta$ .

step 3.1step 1.2L1L4L5

5.1

Step 4.1 holds for every $x \in X$ , so $2\eta$ bounds the values $\bar d(f_n(x),f(x))$ above and hence $\bar\rho(f_n,f) \le 2\eta \le \varepsilon/2 < \varepsilon$ , for every $n \ge K$ .

step 1.2step 4.1L1

6.1

As $\varepsilon$ was an arbitrary positive real, step 5.1 says $f_n \to f$ in $(Y^{X},\bar\rho)$ ; so every $\bar\rho$ -Cauchy sequence converges in $Y^{X}$ , which is claim 1.

step 5.1L4

7.1

For claim 2, $C(X,Y)$ is closed in the complete space $(Y^{X},\bar\rho)$ , so the metric subspace $C(X,Y)$ with the restriction of $\bar\rho$ is complete.

step 6.1L6L7∎

Remarks

What completeness of the target buys, pointwise and then uniformly. Step 3.1 produces the limit function pointwise, and that step alone would hold for a merely pointwise Cauchy condition. What the uniform Cauchy condition adds is step 5.1: the same $\eta$ works at every $x$ , so the bound on $\bar d(f_n(x),f(x))$ is uniform in $x$ and therefore bounds the supremum.
Step 4.1 chooses nothing. For each fixed $x$ an index $m$ is instantiated and used inside the same sentence; the conclusion $\bar d(f_n(x),f(x)) < 2\eta$ does not mention $m$ , so no function $x \mapsto m$ is ever formed. That is the standard way this library avoids a spurious countable choice.
Completeness is a property of the metric, not of the topology (Complete metric space: every Cauchy sequence converges in the space), and the metric here is $\bar\rho$ , built from the truncation $\bar d = \min\{d,1\}$ . A different metric inducing the same topology on $Y$ need not make $Y$ complete, and then nothing above applies; the hypothesis is that $(Y,d)$ itself is complete.
The classical special case. With $Y = \mathbb{R}$ this says that the bounded-or-not real functions on a nonempty set are complete in the uniform metric, and that the continuous ones form a closed, hence complete, subspace. The companion page works $C([0,1],\mathbb{R})$ explicitly and compares the uniform metric there with the supremum metric of The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set.

Depends on

Used by

C([0,1], ℝ) is complete, and on it the uniform metric and the supremum metric induce the same topology Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 139 results over 37 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

Uniform convergence (Wikipedia) (standard reference, not scraped)
Complete metric space (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §43 (standard reference, not scraped)

If (Y,d)(Y,d)(Y,d) is complete then YXY^{X}YX is complete in the uniform metric, and so is C(X,Y)C(X,Y)C(X,Y)