LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

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}^n$ as the set of functions $n \to \mathbb{R}$ , and $d_1$ , $d_2$ , $d_\infty$ are metrics on it

Statement

Let $n \in \mathbb{N}$ with $n \ge 1$ . A von Neumann natural is the set of its predecessors, $n = \{0, 1, \dots, n-1\}$ (The natural numbers $\mathbb{N}$ (von Neumann)), so it can be used directly as an index set. Define

$\mathbb{R}^n := \{\, x : x \text{ is a function } n \to \mathbb{R} \,\},$

and write $x_k$ for $x(k)$ , $k < n$ . Two elements of $\mathbb{R}^n$ are equal exactly when they agree at every $k < n$ , functions being equal when they have the same values. For $x, y \in \mathbb{R}^n$ put

$d_1(x,y) := \sum_{k<n} |x_k - y_k|, \qquad d_2(x,y) := \sqrt{\ \sum_{k<n} (x_k - y_k)^2\ }, \qquad d_\infty(x,y) := \max\{\, |x_k - y_k| : k < n \,\}.$

All three are well defined: the finite sums are those of Finite sums and finite products, by recursion; the sum of squares is nonnegative (Laws of finite sums and finite products, Squares of nonzero elements are positive) so it has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ); and $\{|x_k - y_k| : k < n\}$ is a nonempty finite subset of $\mathbb{R}$ , because $n \ge 1$ , so it has a maximum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Then $d_1$ , $d_2$ and $d_\infty$ are metrics on $\mathbb{R}^n$ (Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

Why $n \ge 1$ . For $n = 0$ the set $\mathbb{R}^0$ has exactly one element, the empty function, and $d_1$ and $d_2$ are the empty sum $0$ and its root; but $d_\infty$ would be the maximum of the empty set, which does not exist. The hypothesis $n \ge 1$ is therefore not decoration, and it is carried by every statement about $d_\infty$ in this library.

Facts & Assumptions

Given: A natural $n \ge 1$ ; elements $x, y, z \in \mathbb{R}^n$ ; and the lists $a_k := x_k - y_k$ , $b_k := y_k - z_k$ for $k < n$ , so that $a_k + b_k = x_k - z_k$ . Write $A := \sum_{k<n} a_k^2$ , $C := \sum_{k<n} b_k^2$ and $B := \sum_{k<n} a_k b_k$ .

[L1]

Laws of finite sums (Laws of finite sums and finite products, Finite sums and finite products, by recursion): additivity, scaling, monotonicity; a sum of nonnegative terms is nonnegative, every single term is at most the sum, and a sum of nonnegative terms that vanishes has every term $0$ .

[L2]

Absolute value (Basic properties of the absolute value, Absolute value in an ordered field): $|u| \ge 0$ ; $|u| = 0$ if and only if $u = 0$ ; $|-u| = |u|$ ; and $u \le |u|$ .

[L3]

Two-term triangle inequality: $|u + v| \le |u| + |v|$ (The triangle inequality).

[L4]

Minkowski's inequality at the rational exponent $p = 1$ (Minkowski's inequality for finite sums (rational exponent)): $\sum_{k<n}|a_k + b_k| \le \sum_{k<n}|a_k| + \sum_{k<n}|b_k|$ .

[L5]

Cauchy-Schwarz in root form (The Cauchy-Schwarz inequality for finite sums): $\big|\sum_{k<n} a_k b_k\big| \le \sqrt{\sum_{k<n} a_k^2}\ \sqrt{\sum_{k<n} b_k^2}$ .

[L6]

Square roots (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ): every $c \ge 0$ has a unique $\sqrt{c} \ge 0$ with $(\sqrt{c})^2 = c$ ; in particular $\sqrt{c} = 0$ if and only if $c = 0$ .

[L7]

Squares (Squares of nonzero elements are positive, Integer powers $a^m$ ): $u^2 \ge 0$ always, and $u^2 = 0$ only for $u = 0$ ; and monotonicity of squaring on the nonnegatives, $s \le t \iff s^2 \le t^2$ for $s, t \ge 0$ (Squaring is monotone on the nonnegatives).

[L8]

Maximum of a nonempty finite set of reals: it exists, it belongs to the set, and it is an upper bound of the set (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L9]

Order arithmetic in $\mathbb{R}$ : inequalities may be added and a constant added to both sides, in the strict form of Order is preserved by adding a constant and by adding inequalities and, together with the case of equality settled by totality (Ordered field, Complete ordered field (least-upper-bound property)), in the nonstrict form used below.

Proof

technique · direct

1.1

Separation for $d_1$ : $d_1(x,y) = \sum_{k<n}|a_k|$ is a sum of nonnegative terms, so it vanishes exactly when every $|a_k|$ vanishes, that is exactly when $x_k = y_k$ for all $k < n$ , that is exactly when $x = y$ .

L1L2

1.2

Separation for $d_2$ : $d_2(x,y) = \sqrt{A}$ vanishes exactly when $A = 0$ ; $A$ is a sum of nonnegative terms, so $A = 0$ exactly when $a_k^2 = 0$ for every $k < n$ , which happens exactly when every $a_k = 0$ , that is exactly when $x = y$ .

L1L6L7

1.3

Separation for $d_\infty$ : the maximum $d_\infty(x,y)$ belongs to $\{|a_k| : k < n\}$ and bounds it above, so it is $0$ exactly when every $|a_k| = 0$ , that is exactly when $x = y$ .

L2L8

1.4

L2L7

1.5

Triangle inequality for $d_1$ : applying [L4] to the lists $(a_k)$ and $(b_k)$ gives $d_1(x,z) = \sum_{k<n}|a_k + b_k| \le \sum_{k<n}|a_k| + \sum_{k<n}|b_k| = d_1(x,y) + d_1(y,z)$ .

1.6

Expanding with additivity and scaling: $\sum_{k<n}(a_k + b_k)^2 = \sum_{k<n}\big(a_k^2 + 2a_kb_k + b_k^2\big) = A + 2B + C$ .

L1algebra

1.7

By [L5] and $B \le |B|$ : $B \le \sqrt{A}\,\sqrt{C}$ , and $A = (\sqrt{A})^2$ , $C = (\sqrt{C})^2$ with $\sqrt{A}, \sqrt{C} \ge 0$ .

L2L5L6

1.8

Triangle inequality for $d_\infty$ : for each $k < n$ , $|a_k + b_k| \le |a_k| + |b_k| \le d_\infty(x,y) + d_\infty(y,z)$ because the two maxima bound their sets; so $d_\infty(x,y) + d_\infty(y,z)$ is an upper bound of $\{|a_k + b_k| : k < n\}$ , and the maximum $d_\infty(x,z)$ of that set is one of its elements, whence $d_\infty(x,z) \le d_\infty(x,y) + d_\infty(y,z)$ .

L3L8L9

2.1

Combining steps 1.6 and 1.7: $\sum_{k<n}(a_k+b_k)^2 = A + 2B + C \le (\sqrt{A})^2 + 2\sqrt{A}\sqrt{C} + (\sqrt{C})^2 = \big(\sqrt{A} + \sqrt{C}\big)^2$ .

step 1.6step 1.7L9algebra

3.1

Both $d_2(x,z) = \sqrt{\sum_{k<n}(a_k+b_k)^2}$ and $\sqrt{A} + \sqrt{C}$ are nonnegative, and by step 2.1 the square of the first is at most the square of the second, so monotonicity of squaring on the nonnegatives gives $d_2(x,z) \le \sqrt{A} + \sqrt{C} = d_2(x,y) + d_2(y,z)$ .

step 2.1L6L7

4.1

Each of $d_1$ , $d_2$ , $d_\infty$ satisfies (M1) by steps 1.1, 1.2 and 1.3, satisfies (M2) by step 1.4, and satisfies (M3) by steps 1.5, 3.1 and 1.8 respectively; hence all three are metrics on $\mathbb{R}^n$ .

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.8step 3.1∎

Remarks

$\mathbb{R}^n$ is defined ZFC-natively here, as the set of functions from the von Neumann natural $n$ to $\mathbb{R}$ , precisely so that its coordinates are indexed by $k < n$ and the finite-sum machinery of Finite sums and finite products, by recursion, Minkowski's inequality for finite sums (rational exponent) and The Cauchy-Schwarz inequality for finite sums, all of which sum over $k < n$ , applies without any reindexing.
No rational power appears anywhere above. The triangle inequality for $d_2$ is obtained from Cauchy-Schwarz and the existence of square roots, not from Minkowski at $p = 2$ , so this lemma does not depend on the theory of rational exponents. Minkowski is used only at $p = 1$ , where its statement is the termwise sum of the two-term triangle inequality.
The three metrics are Lipschitz equivalent, with explicit constants, and in particular have the same topology; that computation is on the companion page and is not needed here.

Depends on

Used by

…and 2 more results.

Dependency tree · next 3 levels

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

Euclidean space (Wikipedia) (standard reference, not scraped)
Taxicab geometry (Wikipedia) (standard reference, not scraped)
Lp space (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)
R. Gardner, Introduction to Topology, notes on Munkres Section 20: The Metric Topology (East Tennessee State University) (standard reference, not scraped)

Rn\mathbb{R}^nRn as the set of functions n→Rn \to \mathbb{R}n→R, and d1d_1d1​, d2d_2d2​, d∞d_\inftyd∞​ are metrics on it