Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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 ∥⋅∥p is a norm on Rn, and the induced metrics are exactly d1, d2 and d∞ of the published metric-spaces page

Statement

Let n∈N and let p∈Q with p≥1, with the norms of The p-norms ∥x∥p for rational p≥1, and ∥x∥∞. Then:

  1. ∥⋅∥p is a norm on Rn (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).
  2. For n≥1, ∥⋅∥∞ is a norm on Rn.
  3. The dictionary. For n≥1 and all x,y∈Rn, ∥x−y∥1=d1(x,y),∥x−y∥2=d2(x,y),∥x−y∥∞=d∞(x,y), where d1, d2, d∞ are the metrics of the published Rn as the set of functions n→R, and d1, d2, d∞ 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 (Rn,d2) of the published metric-spaces page and the metric space underlying the normed space (Rn,∥⋅∥2) of this page are the same object. Hence completeness (R and Rn for n≥1 with the Euclidean metric are complete, componentwise from the Cauchy criterion in R clause 2), Heine-Borel (Heine-Borel in Rn: with the Euclidean metric a subset of Rn 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≥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 Rn 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≥1, vectors x,y∈Rn and a real λ; write S(x):=∑k<n∣xk∣p, so that ∥x∥p=S(x)1/p (The p-norms ∥x∥p for rational p≥1, and ∥x∥∞, Finite sums and finite products, by recursion).

[L1]

Rational powers (Rational powers ar of a positive base, Laws of rational exponents): for a,b≥0 and rationals r,s>0 one has ar≥0, (ab)r=arbr, 0r=0, and ar>0 when a>0; and for a>0, (ar)s=ars and a1=a.

[L2]

Monotonicity in the base (Monotonicity of r↦ar and of a↦ar clause 2): for a rational r>0 and reals 0≤a<b one has ar<br; hence a≤b implies ar≤br, the case a=b being trivial, and ar=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≥1 (Minkowski's inequality for finite sums (rational exponent)): (∑k<n∣ak+bk∣p)1/p≤(∑k<n∣ak∣p)1/p+(∑k<n∣bk∣p)1/p.

[L5]

Absolute value (Basic properties of the absolute value, Absolute value in an ordered field, The triangle inequality): ∣t∣≥0; ∣t∣=0 exactly when t=0; ∣st∣=∣s∣ ∣t∣; ∣s+t∣≤∣s∣+∣t∣; and ∣t∣2=t2.

[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 ≤ is transitive (Ordered field).

[L9]

The published metrics on Rn for n≥1 are d1(x,y)=∑k<n∣xk−yk∣, d2(x,y)=∑k<n(xk−yk)2 and d∞(x,y)=max⁡{∣xk−yk∣:k<n}, and each is a metric (Rn as the set of functions n→R, and d1, d2, d∞ 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 ∣xk∣p is nonnegative, so S(x)≥0 and ∥x∥p=S(x)1/p is defined and nonnegative.

L1L3
1.2

S(x)=0 holds exactly when ∣xk∣p=0 for every k<n, a vanishing sum of nonnegative terms having every term 0; and ∣xk∣p=0 exactly when ∣xk∣=0, that is exactly when xk=0.

L1L2L3L5
1.3

For every k<n, ∣(λx)k∣p=(∣λ∣ ∣xk∣)p=∣λ∣p∣xk∣p, so S(λx)=∣λ∣pS(x) by scaling of finite sums.

L1L3L5
1.4

Instantiating [L4] at ak:=xk and bk:=yk, and using (x+y)k=xk+yk, gives ∥x+y∥p≤∥x∥p+∥y∥p, which is axiom (N3) for ∥⋅∥p.

L4L8
1.5

Under [A1] the set {∣xk∣:k<n} is nonempty and finite, so ∥x∥∞ exists, is one of the ∣xk∣, and satisfies ∣xk∣≤∥x∥∞ for every k<n; in particular ∥x∥∞≥0.

A1L5L6
1.6

Under [A1], ∥x−y∥1=∑k<n∣xk−yk∣ by the case p=1 of the definition, and that is the written expression for d1(x,y).

L1L9
1.7

Under [A1], ∥x−y∥2=(∑k<n∣xk−yk∣2)1/2=∑k<n(xk−yk)2, using ∣t∣2=t2 and the identification of the exponent 1/2 with the nonnegative square root, and that is the written expression for d2(x,y).

L5L8L9
1.8

Under [A1], ∥x−y∥∞=max⁡{∣xk−yk∣:k<n} by definition, and that is the written expression for d∞(x,y).

L9
2.1

∥x∥p=0 holds exactly when S(x)=0, since S(x)>0 would give S(x)1/p>0 and 01/p=0.

step 1.1L1L2
2.2

Under [A1]: ∥x∥∞=0 forces ∣xk∣≤0 and ∣xk∣≥0 for every k<n, hence x=0; and ∥0∥∞=0. This is (N1) for ∥⋅∥∞.

step 1.5L5L8
2.3

Under [A1]: for every k<n, ∣(λx)k∣=∣λ∣ ∣xk∣≤∣λ∣ ∥x∥∞, and choosing j<n with ∣xj∣=∥x∥∞ gives ∣(λx)j∣=∣λ∣ ∥x∥∞; so ∣λ∣∥x∥∞ belongs to the set and bounds it above, whence ∥λx∥∞=∣λ∣∥x∥∞. This is (N2) for ∥⋅∥∞.

step 1.5L5L6L7
2.4

Under [A1]: for every k<n, ∣(x+y)k∣=∣xk+yk∣≤∣xk∣+∣yk∣≤∥x∥∞+∥y∥∞; choosing j<n with ∣(x+y)j∣=∥x+y∥∞ gives ∥x+y∥∞≤∥x∥∞+∥y∥∞, which is (N3) for ∥⋅∥∞.

step 1.5L5L6L7
3.1

By steps 2.1 and 1.2, ∥x∥p=0 exactly when xk=0 for every k<n, that is exactly when x=0; this is axiom (N1) for ∥⋅∥p.

step 2.1step 1.2L8
3.2

Steps 2.2, 2.3 and 2.4 are (N1), (N2) and (N3) for ∥⋅∥∞ under [A1], so clause 2 holds.

step 2.2step 2.3step 2.4A1L8
4.1

If λ=0 then λx=0 and both sides of (N2) are 0 by step 3.1; if λ≠0 then ∣λ∣>0, and step 1.3 with the power laws gives ∥λx∥p=(∣λ∣pS(x))1/p=(∣λ∣p)1/pS(x)1/p=∣λ∣p⋅(1/p)∥x∥p=∣λ∣ ∥x∥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 ∥⋅∥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 ∥⋅∥2 on Rn for n≥1 is the published d2, which is the consequence recorded in the Statement.

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

Remarks

Depends on

Used by

…and 4 more results.

Dependency tree · two levels

97 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