TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

$R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$

Statement

$(R, d_{R})$ with the usual metric $d_{R} (x, y) = ∣ x - y ∣$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded) is a complete metric space (Complete metric space: every Cauchy sequence converges in the space).
Let $n \in N$ with $n \geq 1$ and let $d_{2}$ be the Euclidean metric on $R^{n}$ ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it). Then $(R^{n}, d_{2})$ is complete.

The hypothesis $n \geq 1$ is inherited and is not decoration. $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it defines $R^{n}$ and its three metrics only for $n \geq 1$ , because at $n = 0$ the metric $d_{\infty}$ would be a maximum over the empty index set. Every statement about $R^{n}$ in this library carries the hypothesis, and this one does too.

Facts & Assumptions

Given: A natural $n \geq 1$ ; $R^{n}$ is the set of functions $n \to R$ with $d_{2} (x, y) = \sqrt{\sum_{k < n} (x_{k} - y_{k})^{2}}$ ; a real $ε > 0$ .

[A1]

Cauchy criterion in $R$ : every Cauchy sequence of reals converges to a real (The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges, Limits and Cauchy sequences of reals).

[L1]

The usual metric of $R$ is $d_{R} (x, y) = ∣ x - y ∣$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded).

[L2]

Convergence in a metric space: $x_{k} \to p$ in $(X, d)$ means $d (x_{k}, p) \to 0$ in $R$ ; Cauchyness means $d (x_{m}, x_{n}) < ε$ for $m, n$ beyond an index (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Cauchy sequence in a metric space, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L3]

$d_{2}$ is a metric on $R^{n}$ for $n \geq 1$ , its defining sum is a finite sum, and the sum of squares is nonnegative with a unique nonnegative square root ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Finite sums and finite products, by recursion, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[L4]

Finite sums of nonnegative terms dominate each term and are monotone, and $\sum_{k < n} λ = n λ$ (Laws of finite sums and finite products, claims 2 and 4).

[L5]

For $a, b \geq 0$ : $a \leq b ⟺ a^{2} \leq b^{2}$ and $a < b ⟺ a^{2} < b^{2}$ (Squaring is monotone on the nonnegatives); and $∣ t ∣^{2} = t^{2}$ for every real $t$ (Basic properties of the absolute value).

[L6]

A nonempty finite set of naturals has a maximum, and every nonempty set of naturals has a least element (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set, The well-ordering principle).

[L7]

$n \geq 1$ gives $0 < 1 / n \leq 1$ and $0 < ε / (2 n)$ (Inverses of positives are positive, and reciprocation reverses order).

[L8]

Limits of real sequences are unique, which is what licenses writing $\lim_{k} x_{k}$ for a sequence already known to converge (A sequence has at most one limit).

Proof

technique · direct

1.1

By [L1] a sequence $(x_{k})$ of reals is Cauchy in $(R, d_{R})$ exactly when $∣ x_{m} - x_{n} ∣ < ε$ for all $m, n$ beyond an index and every rational $ε > 0$ , which is verbatim the Cauchy condition of Limits and Cauchy sequences of reals; and $x_{k} \to p$ in $(R, d_{R})$ exactly when $∣ x_{k} - p ∣ \to 0$ , which is verbatim convergence to $p$ there.

L1L2

1.2

Let $x, y \in R^{n}$ and $j < n$ . The terms $(x_{k} - y_{k})^{2}$ are nonnegative, so $(x_{j} - y_{j})^{2} \leq \sum_{k < n} (x_{k} - y_{k})^{2} = d_{2} (x, y)^{2}$ ; both $∣ x_{j} - y_{j} ∣$ and $d_{2} (x, y)$ are nonnegative and $∣ x_{j} - y_{j} ∣^{2} = (x_{j} - y_{j})^{2}$ , so $∣ x_{j} - y_{j} ∣ \leq d_{2} (x, y)$ .

L3L4L5

1.3

Let $x, y \in R^{n}$ satisfy $∣ x_{j} - y_{j} ∣ < ε / (2 n)$ for every $j < n$ . Then $(x_{j} - y_{j})^{2} \leq (ε / (2 n))^{2}$ for every $j < n$ , so $d_{2} (x, y)^{2} \leq n \cdot ε^{2} / (4 n^{2}) = ε^{2} / (4 n) \leq ε^{2} / 4 < ε^{2}$ , and therefore $d_{2} (x, y) < ε$ .

L3L4L5L7

2.1

Claim 1: let $(x_{k})$ be a Cauchy sequence in $(R, d_{R})$ . By step 1.1 it is a Cauchy sequence of reals, so by [A1] it converges to some $x \in R$ , and by step 1.1 again $x_{k} \to x$ in $(R, d_{R})$ . Hence every Cauchy sequence in $(R, d_{R})$ converges in it.

step 1.1A1L2

2.2

Now let $(x^{(k)})$ be a Cauchy sequence in $(R^{n}, d_{2})$ and fix $j < n$ . By step 1.2, $∣ x_{j}^{(m)} - x_{j}^{(l)} ∣ \leq d_{2} (x^{(m)}, x^{(l)})$ for all $m, l$ , so the real sequence $(x_{j}^{(k)})_{k}$ is Cauchy, and by [A1] it converges; its limit is unique, so the notation $y_{j} : = \lim_{k} x_{j}^{(k)}$ denotes a single real.

step 1.2A1L2L8

3.1

The assignment $j \mapsto y_{j}$ is a function $n \to R$ , hence an element $y \in R^{n}$ ; no choice is used, because $y_{j}$ is the unique limit of the $j$ -th coordinate sequence.

step 2.2L3construct

3.2

For each $j < n$ let $K_{j}$ be the least natural such that $∣ x_{j}^{(k)} - y_{j} ∣ < ε / (2 n)$ for all $k \geq K_{j}$ , which exists because the coordinate sequence converges to $y_{j}$ and every nonempty set of naturals has a least element; and put $K : = \max {K_{j} : j < n}$ , a maximum of a nonempty finite set of naturals since $n \geq 1$ .

step 2.2L6L7choose

4.1

For every $k \geq K$ and every $j < n$ we have $k \geq K_{j}$ , hence $∣ x_{j}^{(k)} - y_{j} ∣ < ε / (2 n)$ , and therefore $d_{2} (x^{(k)}, y) < ε$ by step 1.3.

step 1.3step 3.1step 3.2

5.1

Since $ε > 0$ was an arbitrary real, $x^{(k)} \to y$ in $(R^{n}, d_{2})$ with $y \in R^{n}$ ; so every Cauchy sequence in $(R^{n}, d_{2})$ converges in it, which with step 2.1 gives claims 1 and 2.

step 2.1step 4.1L2∎

Remarks

The proof is the Cauchy criterion plus two inequalities. Step 1.2 says a coordinate difference is at most the Euclidean distance, which turns a Cauchy sequence of points into $n$ Cauchy sequences of reals; step 1.3 says that coordinates uniformly below $ε / (2 n)$ force the Euclidean distance below $ε$ , which turns $n$ convergent coordinate sequences back into one convergent sequence of points. Nothing else about $R^{n}$ is used, and in particular the Cauchy-Schwarz inequality is not needed here.
The same two inequalities hold for $d_{1}$ and $d_{\infty}$ , with the same proof of completeness. For $d_{1} (x, y) = \sum_{k < n} ∣ x_{k} - y_{k} ∣$ : each term is at most the sum (Laws of finite sums and finite products), so $∣ x_{j} - y_{j} ∣ \leq d_{1} (x, y)$ ; and $∣ x_{j} - y_{j} ∣ < ε / (2 n)$ for all $j < n$ gives $d_{1} (x, y) \leq n ε / (2 n) = ε / 2 < ε$ . For $d_{\infty} (x, y) = \max {∣ x_{k} - y_{k} ∣ : k < n}$ : the maximum dominates each entry and is one of them (Every nonempty finite set of reals has a maximum and a minimum), so $∣ x_{j} - y_{j} ∣ \leq d_{\infty} (x, y)$ , and entries all below $ε / 2$ make the maximum at most $ε / 2$ . Substituting either pair of inequalities for steps 1.2 and 1.3 leaves the rest of the proof unchanged, so $(R^{n}, d_{1})$ and $(R^{n}, d_{\infty})$ are complete as well. Nothing later on this page uses that.
No choice is spent. The limit point $y$ is assembled coordinatewise in step 3.1 from limits that are unique, and the finitely many indices $K_{j}$ of step 3.2 are made canonical by taking the least one. This matters because completeness proofs elsewhere on this page do spend ${A C}_{ω}$ , and the contrast is worth keeping visible.
Where the least-upper-bound property is. Entirely inside The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges. This theorem is a transfer result: it moves completeness from $R$ to $R^{n}$ and adds no new content about the reals.

Depends on

Used by

Dependency tree · two levels

63 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

Complete metric space (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)

RR and RnRn for n≥1n≥1 with the Euclidean metric are complete, componentwise from the Cauchy criterion in RR