LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)

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.

Each $\lVert\cdot\rVert_p$ is a norm on $\mathbb{R}^n$ , and the induced metrics are exactly $d_1$ , $d_2$ and $d_\infty$ of the published metric-spaces page

Statement

Let $n \in \mathbb{N}$ and let $p \in \mathbb{Q}$ with $p \ge 1$ , with the norms of The $p$ -norms $\lVert x\rVert_p$ for rational $p \ge 1$ , and $\lVert x\rVert_\infty$ . Then:

$\lVert\cdot\rVert_p$ is a norm on $\mathbb{R}^{n}$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).
For $n \ge 1$ , $\lVert\cdot\rVert_\infty$ is a norm on $\mathbb{R}^{n}$ .
The dictionary. For $n \ge 1$ and all $x, y \in \mathbb{R}^{n}$ , $\lVert x-y\rVert_1 = d_1(x,y), \qquad \lVert x-y\rVert_2 = d_2(x,y), \qquad \lVert x-y\rVert_\infty = d_\infty(x,y),$ where $d_1$ , $d_2$ , $d_\infty$ are the metrics of the published $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$ , and $d_1$ , $d_2$ , $d_\infty$ are metrics on it. So the metric induced by each of these three norms (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms) is the correspondingly named published metric, not merely one equivalent to it.

Consequence, used repeatedly below and stated once here. By clause 3 at $p = 2$ , the metric space $(\mathbb{R}^{n}, d_2)$ of the published metric-spaces page and the metric space underlying the normed space $(\mathbb{R}^{n}, \lVert\cdot\rVert_2)$ of this page are the same object. Hence completeness ( $\mathbb{R}$ and $\mathbb{R}^n$ for $n \ge 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $\mathbb{R}$ clause 2), Heine-Borel (Heine-Borel in $\mathbb{R}^n$ : with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line clause 2) and the compactness equivalences (For a metric space, compact, countably compact, limit point compact, sequentially compact, and complete together with totally bounded are all equivalent, given countable choice and dependent choice) are statements about this page's normed space, with their hypothesis $n \ge 1$ inherited unchanged and not weakened. Nothing below cites any of those three theorems for $n = 0$ .

Why this lemma exists. Without it the library would hold a norm-induced metric on $\mathbb{R}^{n}$ and a separately published metric on the same set with no recorded relation, and every later citation would have to guess which was meant. The proof of clause 3 is a comparison of two written expressions; the value is that the comparison is made and recorded.

Facts & Assumptions

Given: A natural number $n$ , a rational $p \ge 1$ , vectors $x, y \in \mathbb{R}^{n}$ and a real $\lambda$ ; write $S(x) := \sum_{k<n}|x_k|^{p}$ , so that $\lVert x\rVert_p = S(x)^{1/p}$ (The $p$ -norms $\lVert x\rVert_p$ for rational $p \ge 1$ , and $\lVert x\rVert_\infty$ , Finite sums and finite products, by recursion).

[A1]

For clauses 2 and 3, $n \ge 1$ , so that $\{|x_k| : k<n\}$ is a nonempty finite set of reals (The $p$ -norms $\lVert x\rVert_p$ for rational $p \ge 1$ , and $\lVert x\rVert_\infty$ , $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$ , and $d_1$ , $d_2$ , $d_\infty$ are metrics on it).

[L1]

Rational powers (Rational powers $a^r$ of a positive base, Laws of rational exponents): for $a, b \ge 0$ and rationals $r, s > 0$ one has $a^{r} \ge 0$ , $(ab)^{r} = a^{r}b^{r}$ , $0^{r} = 0$ , and $a^{r} > 0$ when $a > 0$ ; and for $a > 0$ , $(a^{r})^{s} = a^{rs}$ and $a^{1} = a$ .

[L2]

Monotonicity in the base (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ clause 2): for a rational $r > 0$ and reals $0 \le a < b$ one has $a^{r} < b^{r}$ ; hence $a \le b$ implies $a^{r} \le b^{r}$ , the case $a = b$ being trivial, and $a^{r} = 0$ only for $a = 0$ .

[L3]

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, each single term is at most such a sum, and a sum of nonnegative terms that vanishes has every term $0$ .

[L4]

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

[L5]

Absolute value (Basic properties of the absolute value, Absolute value in an ordered field, The triangle inequality): $|t| \ge 0$ ; $|t| = 0$ exactly when $t = 0$ ; $|st| = |s|\,|t|$ ; $|s+t| \le |s|+|t|$ ; and $|t|^{2} = t^{2}$ .

[L6]

Maxima (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set): a nonempty finite set of reals has a maximum, the maximum belongs to the set and bounds it above, and a set with an upper bound belonging to it has that element as its maximum.

[L7]

Order arithmetic: multiplying an inequality by a nonnegative real preserves it (Sign rules for products and monotonicity of multiplication in its strict form, together with the case of equality settled by totality), and $\le$ is transitive (Ordered field).

[L8]

The norm axioms (N1), (N2), (N3) (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms); $\lVert\cdot\rVert_2$ agrees with the Euclidean norm of The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$ , and is a norm by Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$ , the parallelogram law and polarisation; square roots are the rational power at exponent $1/2$ (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ , The $p$ -norms $\lVert x\rVert_p$ for rational $p \ge 1$ , and $\lVert x\rVert_\infty$ ).

[L9]

The published metrics on $\mathbb{R}^{n}$ for $n \ge 1$ are $d_1(x,y) = \sum_{k<n}|x_k-y_k|$ , $d_2(x,y) = \sqrt{\sum_{k<n}(x_k-y_k)^{2}}$ and $d_\infty(x,y) = \max\{|x_k-y_k| : k<n\}$ , and each is a metric ( $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$ , and $d_1$ , $d_2$ , $d_\infty$ are metrics on it, Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Proof

technique · direct

1.1

Every term $|x_k|^{p}$ is nonnegative, so $S(x) \ge 0$ and $\lVert x\rVert_p = S(x)^{1/p}$ is defined and nonnegative.

L1L3

1.2

$S(x) = 0$ holds exactly when $|x_k|^{p} = 0$ for every $k<n$ , a vanishing sum of nonnegative terms having every term $0$ ; and $|x_k|^{p} = 0$ exactly when $|x_k| = 0$ , that is exactly when $x_k = 0$ .

L1L2L3L5

1.3

For every $k<n$ , $|(\lambda x)_k|^{p} = \bigl(|\lambda|\,|x_k|\bigr)^{p} = |\lambda|^{p}|x_k|^{p}$ , so $S(\lambda x) = |\lambda|^{p}S(x)$ by scaling of finite sums.

L1L3L5

1.4

Instantiating [L4] at $a_k := x_k$ and $b_k := y_k$ , and using $(x+y)_k = x_k+y_k$ , gives $\lVert x+y\rVert_p \le \lVert x\rVert_p + \lVert y\rVert_p$ , which is axiom (N3) for $\lVert\cdot\rVert_p$ .

L4L8

1.5

Under [A1] the set $\{|x_k| : k<n\}$ is nonempty and finite, so $\lVert x\rVert_\infty$ exists, is one of the $|x_k|$ , and satisfies $|x_k| \le \lVert x\rVert_\infty$ for every $k<n$ ; in particular $\lVert x\rVert_\infty \ge 0$ .

A1L5L6

1.6

Under [A1], $\lVert x-y\rVert_1 = \sum_{k<n}|x_k-y_k|$ by the case $p=1$ of the definition, and that is the written expression for $d_1(x,y)$ .

L1L9

1.7

Under [A1], $\lVert x-y\rVert_2 = \bigl(\sum_{k<n}|x_k-y_k|^{2}\bigr)^{1/2} = \sqrt{\sum_{k<n}(x_k-y_k)^{2}}$ , using $|t|^{2} = t^{2}$ and the identification of the exponent $1/2$ with the nonnegative square root, and that is the written expression for $d_2(x,y)$ .

L5L8L9

1.8

Under [A1], $\lVert x-y\rVert_\infty = \max\{|x_k-y_k| : k<n\}$ by definition, and that is the written expression for $d_\infty(x,y)$ .

2.1

$\lVert x\rVert_p = 0$ holds exactly when $S(x) = 0$ , since $S(x) > 0$ would give $S(x)^{1/p} > 0$ and $0^{1/p} = 0$ .

step 1.1L1L2

2.2

Under [A1]: $\lVert x\rVert_\infty = 0$ forces $|x_k| \le 0$ and $|x_k| \ge 0$ for every $k<n$ , hence $x = 0$ ; and $\lVert 0\rVert_\infty = 0$ . This is (N1) for $\lVert\cdot\rVert_\infty$ .

step 1.5L5L8

2.3

step 1.5L5L6L7

2.4

Under [A1]: for every $k<n$ , $|(x+y)_k| = |x_k+y_k| \le |x_k| + |y_k| \le \lVert x\rVert_\infty + \lVert y\rVert_\infty$ ; choosing $j<n$ with $|(x+y)_j| = \lVert x+y\rVert_\infty$ gives $\lVert x+y\rVert_\infty \le \lVert x\rVert_\infty + \lVert y\rVert_\infty$ , which is (N3) for $\lVert\cdot\rVert_\infty$ .

step 1.5L5L6L7

3.1

By steps 2.1 and 1.2, $\lVert x\rVert_p = 0$ exactly when $x_k = 0$ for every $k<n$ , that is exactly when $x = 0$ ; this is axiom (N1) for $\lVert\cdot\rVert_p$ .

step 2.1step 1.2L8

3.2

Steps 2.2, 2.3 and 2.4 are (N1), (N2) and (N3) for $\lVert\cdot\rVert_\infty$ under [A1], so clause 2 holds.

step 2.2step 2.3step 2.4A1L8

4.1

If $\lambda = 0$ then $\lambda x = 0$ and both sides of (N2) are $0$ by step 3.1; if $\lambda \ne 0$ then $|\lambda| > 0$ , and step 1.3 with the power laws gives $\lVert \lambda x\rVert_p = \bigl(|\lambda|^{p}S(x)\bigr)^{1/p} = \bigl(|\lambda|^{p}\bigr)^{1/p}S(x)^{1/p} = |\lambda|^{p\cdot(1/p)}\lVert x\rVert_p = |\lambda|\,\lVert x\rVert_p$ ; this is axiom (N2).

step 1.3step 3.1L1L5L8

5.1

Steps 3.1, 4.1 and 1.4 are (N1), (N2) and (N3) for $\lVert\cdot\rVert_p$ , so clause 1 holds.

step 1.4step 3.1step 4.1L8

6.1

Steps 1.6, 1.7 and 1.8 give clause 3, and with steps 5.1 and 3.2 all three clauses are proved; in particular the metric induced by $\lVert\cdot\rVert_2$ on $\mathbb{R}^{n}$ for $n \ge 1$ is the published $d_2$ , which is the consequence recorded in the Statement.

step 5.1step 3.2step 1.6step 1.7step 1.8L9∎

Remarks

What the consequence does and does not license. Because the two metric spaces are literally the same, a published theorem about $(\mathbb{R}^{n}, d_2)$ may be quoted here verbatim. It may not be quoted with a weaker hypothesis: $\mathbb{R}$ and $\mathbb{R}^n$ for $n \ge 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $\mathbb{R}$ , Heine-Borel in $\mathbb{R}^n$ : with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line and $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$ , and $d_1$ , $d_2$ , $d_\infty$ are metrics on it are all stated for $n \ge 1$ only, because $d_\infty$ is a maximum over an empty index set at $n = 0$ , and every item on this page that uses one of them carries $n \ge 1$ in its own statement.
Clause 1 holds at $n = 0$ and clause 2 does not apply there. At $n = 0$ every $\lVert\cdot\rVert_p$ is the zero function on the one-element space $\mathbb{R}^{0}$ , which is the unique norm on the zero space (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms); $\lVert\cdot\rVert_\infty$ is not defined there at all.
The route to (N3) differs between the two families, and that is not an accident. For $\lVert\cdot\rVert_p$ the triangle inequality is Minkowski's inequality, a genuine theorem about rational powers; for $\lVert\cdot\rVert_\infty$ it is the elementary argument of step 2.4, that a maximum of sums is at most the sum of the maxima. The second argument is the one that needs a nonempty index set.

Depends on

Used by

Dependency tree · next 3 levels

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

Lp space (Wikipedia) (standard reference, not scraped)
Minkowski inequality (Wikipedia) (standard reference, not scraped)
J. Demmel, MA221 Lecture 3: Vector Norms (standard reference, not scraped)
G. Zitelli, Math 641 Functional Analysis, Part I (standard reference, not scraped)

Each ∥⋅∥p\lVert\cdot\rVert_p∥⋅∥p​ is a norm on Rn\mathbb{R}^nRn, and the induced metrics are exactly d1d_1d1​, d2d_2d2​ and d∞d_\inftyd∞​ of the published metric-spaces page