LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)

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 standard weighted metric on a countable product of bounded complete metric spaces is complete

Statement

Let $((X_{n}, d_{n}))_{n \in N}$ be complete metric spaces with $d_{n} \leq 1$ . On $\prod_{n} X_{n}$ , the formula $D (x, y) = \sum_{n = 0}^{\infty} 2^{- (n + 1)} d_{n} (x_{n}, y_{n})$ defines a complete metric inducing the product topology. The empty product is the one-point space.

Facts & Assumptions

Given: The complete bounded metric spaces of the statement. No choice principle is assumed: the limits of any supplied coordinate sequences are unique.

[F1]

The product set. Let $I$ be a set and let $X_{i}$ be a set for each $i \in I$ . The product is $\prod_{i \in I} X_{i} : = {x : x is a function with domain I and x (i) \in X_{i} for every i \in I},$ and we write $x_{i} : = x (i)$ , the $i$ -th coordinate of $x$ . Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For $j \in I$ the $j$ -th projection is $π_{j} : \prod_{i \in I} X_{i} \to X_{j}, π_{j} (x) : = x_{j} .$ . The product topology $T^{Π}$ on $\prod_{i} X_{i}$ is the initial topology of the projections: the topology generated by the subbasis ${π_{i}^{- 1} [U] : i \in I, U \in T_{i}}$ . Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes $\prod_{i \in I} U_{i}$ with every $U_{i}$ open in $X_{i}$ and $U_{i} = X_{i}$ for all but finitely many $i$ . (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).

[F2]

Let $(X, d)$ be a metric space (def-metric-space). $(X, d)$ is complete if every Cauchy sequence in $(X, d)$ converges to a point of $X$ ; a subset $A \subseteq X$ is called complete when the metric subspace $(A, d_{A})$ is complete. (Complete metric space: every Cauchy sequence converges in the space).

[F3]

Throughout, $R$ is the complete ordered field (def-real-numbers) and a sequence of reals is a function $a : N \to R$ (def-sequence), written $(a_{k})$ ; recall that $N$ contains $0$ . The sequence of partial sums of a sequence $(a_{k})$ of reals is $s_{n} : = \sum_{k < n} a_{k}$ , so that $s_{0} = 0$ and $s_{n + 1} = s_{n} + a_{n}$ ; the series $\sum a_{k}$ converges when $(s_{n})$ converges, and its sum is then that limit. (Series, partial sums, convergence and the sum, divergence, and the tail series).

[F4]

Let $r \in R$ and let $r^{k}$ be the integer power (def-integer-power), so that $r^{0} = 1$ for every $r$ , including $r = 0$ . 1. If $∣ r ∣ < 1$ then the series $\sum r^{k}$ converges (def-series) and $\sum_{k = 0}^{\infty} r^{k} = \frac{1}{1 - r} .$ 2. If $∣ r ∣ \geq 1$ then $\sum r^{k}$ diverges. The series starts at $k = 0$ and its first term is $r^{0} = 1$ ; in particular $\sum_{k = 0}^{\infty} 2^{- k} = 2$ , while the series starting at $k = 1$ sums to $1$ . Which starting index is meant has to be said, and it is said here. (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

Proof

technique · direct

1.1givenF1F3F4

Put $w_{n} = 2^{- (n + 1)}$ . By [F4], $\sum_{n \geq 0} w_{n} = 1$ and $\sum_{n \geq N} w_{n} = 2^{- N}$ . Since $0 \leq d_{n} (x_{n}, y_{n}) \leq 1$ , the partial sums of $\sum_{n} w_{n} d_{n} (x_{n}, y_{n})$ increase and are bounded by $1$ , so $D (x, y)$ is finite. Symmetry and $D (x, x) = 0$ hold termwise. If $D (x, y) = 0$ , every nonnegative summand vanishes; each $w_{n} > 0$ , hence $d_{n} (x_{n}, y_{n}) = 0$ for every $n$ , and [F1] gives $x = y$ . Summing each coordinate triangle inequality to a finite index and passing to the limit gives $D (x, z) \leq D (x, y) + D (y, z)$ . Thus $D$ is a metric on the product, including when that set is empty.

2.1F1F4step 1.1

For each $j$ , the $j$ th nonnegative summand gives $d_{j} (x_{j}, y_{j}) \leq 2^{j + 1} D (x, y)$ . Hence every coordinate projection is $D$ -continuous, so every product-open set is $D$ -open by [F1]. Conversely, fix $x$ in the product and $ε > 0$ . Choose $N$ with $2^{- N} < ε / 2$ by [F4]. The finite-coordinate box $U = {y : d_{j} (x_{j}, y_{j}) < ε / 2 for j < N}$ is product-open and contains $x$ . For $y \in U$ , its first $N$ summands total less than $ε / 2$ because $\sum_{j < N} w_{j} \leq 1$ , and its remaining summands total at most $2^{- N} < ε / 2$ . Thus $U \subseteq B_{D} (x, ε)$ . Applying this at each point of a $D$ -open set with a ball contained in that set shows the set is product-open. The topologies coincide.

3.1F1F2F4step 1.1step 2.1

Let $(x^{(m)})_{m \geq 0}$ be a $D$ -Cauchy sequence. For every $j$ , the inequality in step 2.1 makes $(x_{j}^{(m)})_{m}$ a $d_{j}$ -Cauchy sequence. Completeness [F2] gives its unique limit $x_{j} \in X_{j}$ . The rule $j \mapsto x_{j}$ therefore defines one element $x$ of the product by [F1]; no choices of limits are made. Given $ε > 0$ , choose $N$ with $2^{- N} < ε / 2$ . For each of the finitely many $j < N$ , coordinate convergence supplies an index $m_{j}$ after which $d_{j} (x_{j}^{(m)}, x_{j}) < ε / 2$ ; take the maximum of these finitely many indices. For all later $m$ , the first $N$ weighted distances total less than $ε / 2$ and the tail is at most $2^{- N} < ε / 2$ . Hence $D (x^{(m)}, x) < ε$ , proving completeness.

4.1F1F3step 1.1step 2.1step 3.1

When the index family itself is empty, [F1] gives the unique empty function as its sole product point; the sum has no terms and is zero, giving the one-point complete metric space and its unique topology. If a countable product has no points, metric and topology assertions are vacuous and no Cauchy sequence exists. These conventions also cover empty coordinate spaces without selecting points in them.

5.1step 1.1step 2.1step 3.1step 4.1∎

Steps 1.1–4.1 establish all asserted metric, topology, completeness, and empty-product clauses.

Depends on

Used by

Dependency tree · two levels

31 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

David Marker, Descriptive Set Theory, §§1–2 (standard reference, not scraped)
Michael Kunzinger, General Topology, §§11.3–11.4 (standard reference, not scraped)
MFF General Topology course summary, §4.3 (standard reference, not scraped)
Jesse Peterson, Real Analysis, §§3.6–3.7 (standard reference, not scraped)