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

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

Statement

$(\mathbb{R}, d_{\mathbb{R}})$ with the usual metric $d_{\mathbb{R}}(x,y) = |x-y|$ (The absolute value makes $\mathbb{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 \mathbb{N}$ with $n \ge 1$ and let $d_2$ be the Euclidean metric on $\mathbb{R}^n$ ( $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$ , and $d_1$ , $d_2$ , $d_\infty$ are metrics on it). Then $(\mathbb{R}^n, d_2)$ is complete.

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

Facts & Assumptions

Given: A natural $n \ge 1$ ; $\mathbb{R}^n$ is the set of functions $n \to \mathbb{R}$ with $d_2(x,y) = \sqrt{\sum_{k<n}(x_k-y_k)^2}$ ; a real $\varepsilon > 0$ .

[A1]

Cauchy criterion in $\mathbb{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 $\mathbb{R}$ is $d_{\mathbb{R}}(x,y) = |x-y|$ (The absolute value makes $\mathbb{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 $\mathbb{R}$ ; Cauchyness means $d(x_m,x_n) < \varepsilon$ 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 $\mathbb{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 $\mathbb{R}^n$ for $n \ge 1$ , its defining sum is a finite sum, and the sum of squares is nonnegative with a unique nonnegative square root ( $\mathbb{R}^n$ as the set of functions $n \to \mathbb{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} \ge 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} \lambda = n\lambda$ (Laws of finite sums and finite products, claims 2 and 4).

[L5]

For $a, b \ge 0$ : $a \le b \iff a^2 \le b^2$ and $a < b \iff 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 \ge 1$ gives $0 < 1/n \le 1$ and $0 < \varepsilon/(2n)$ (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 $(\mathbb{R}, d_{\mathbb{R}})$ exactly when $|x_m - x_n| < \varepsilon$ for all $m,n$ beyond an index and every rational $\varepsilon > 0$ , which is verbatim the Cauchy condition of Limits and Cauchy sequences of reals; and $x_k \to p$ in $(\mathbb{R}, d_{\mathbb{R}})$ exactly when $|x_k - p| \to 0$ , which is verbatim convergence to $p$ there.

L1L2

1.2

Let $x, y \in \mathbb{R}^n$ and $j < n$ . The terms $(x_k - y_k)^2$ are nonnegative, so $(x_j - y_j)^2 \le \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| \le d_2(x,y)$ .

L3L4L5

1.3

Let $x, y \in \mathbb{R}^n$ satisfy $|x_j - y_j| < \varepsilon/(2n)$ for every $j < n$ . Then $(x_j-y_j)^2 \le (\varepsilon/(2n))^2$ for every $j < n$ , so $d_2(x,y)^2 \le n \cdot \varepsilon^2/(4n^2) = \varepsilon^2/(4n) \le \varepsilon^2/4 < \varepsilon^2$ , and therefore $d_2(x,y) < \varepsilon$ .

L3L4L5L7

2.1

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

step 1.1A1L2

2.2

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

step 1.2A1L2L8

3.1

The assignment $j \mapsto y_j$ is a function $n \to \mathbb{R}$ , hence an element $y \in \mathbb{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^{(k)}_j - y_j| < \varepsilon/(2n)$ for all $k \ge 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 \ge 1$ .

step 2.2L6L7choose

4.1

For every $k \ge K$ and every $j < n$ we have $k \ge K_j$ , hence $|x^{(k)}_j - y_j| < \varepsilon/(2n)$ , and therefore $d_2(x^{(k)}, y) < \varepsilon$ by step 1.3.

step 1.3step 3.1step 3.2

5.1

Since $\varepsilon > 0$ was an arbitrary real, $x^{(k)} \to y$ in $(\mathbb{R}^n, d_2)$ with $y \in \mathbb{R}^n$ ; so every Cauchy sequence in $(\mathbb{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 $\varepsilon/(2n)$ force the Euclidean distance below $\varepsilon$ , which turns $n$ convergent coordinate sequences back into one convergent sequence of points. Nothing else about $\mathbb{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| \le d_1(x,y)$ ; and $|x_j-y_j| < \varepsilon/(2n)$ for all $j < n$ gives $d_1(x,y) \le n\varepsilon/(2n) = \varepsilon/2 < \varepsilon$ . 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| \le d_\infty(x,y)$ , and entries all below $\varepsilon/2$ make the maximum at most $\varepsilon/2$ . Substituting either pair of inequalities for steps 1.2 and 1.3 leaves the rest of the proof unchanged, so $(\mathbb{R}^n, d_1)$ and $(\mathbb{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 $\mathrm{AC}_\omega$ , 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 $\mathbb{R}$ to $\mathbb{R}^n$ and adds no new content about the reals.

Depends on

Used by

Dependency tree · next 3 levels

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

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

R\mathbb{R}R and Rn\mathbb{R}^nRn for n≥1n \ge 1n≥1 with the Euclidean metric are complete, componentwise from the Cauchy criterion in R\mathbb{R}R