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.
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
Definition
Throughout this page is the complete ordered field (Complete ordered field (least-upper-bound property)) constructed in this library, in particular a field, so that "vector space" below always means vector space over (Vector space over a field).
Let be a vector space over , with zero vector . A norm on is a function such that for all and all :
- (N1) Separation. if and only if .
- (N2) Absolute homogeneity. , the absolute value being that of Absolute value in an ordered field.
- (N3) Triangle inequality. .
A normed space is a pair consisting of a vector space over and a norm on it. When only one norm is in play we write for ; when several are, the norm is always named.
The values of a norm are real numbers. The codomain is , so is an honest element of the complete ordered field and no infinite value is permitted. The same real-valued codomain is required of a metric by Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric.
Nonnegativity is a theorem, not an axiom
Many texts add a fourth condition . It is redundant. Applying (N2) with gives (Basic properties of the absolute value, In any vector space , , , , and forces or for ), and then (N3) with and gives
where is (N1). So , and if then by addition of inequalities, which trichotomy forbids (Complete ordered field (least-upper-bound property)). Hence for every .
Consequently the verification of a candidate norm has three things to check and not four, exactly as the verification of a candidate metric has three and not four (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric, Nonnegativity of a metric is a consequence of the other axioms, not an axiom). No item in this library assumes nonnegativity of a norm before the argument above.
The induced metric
Let be a norm on and define
where (Vector space over a field). Then is a metric on (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric), and the three axioms are the three conditions above, in order:
- (M1) means , which by (N1) says , that is ; and conversely .
- (M2) , by (N2), Basic properties of the absolute value and (In any vector space , , , , and forces or ).
- (M3) , by (N3).
A normed space is therefore a metric space, and every notion defined for metric spaces — open set (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), convergence, Cauchyness, continuity, compactness — is available in it with no further definition. This library never introduces a second notion of any of them for normed spaces.
Two properties an arbitrary metric need not have
The metric satisfies, for all and :
- translation invariance, ;
- absolute homogeneity, , by (N2).
Not every metric on a vector space arises from a norm, and homogeneity is what fails. The published bounded remetrisation and are metrics uniformly equivalent to , so every metric space carries a bounded metric with the same topology replaces a metric by , a metric with the same topology whose values never exceed ; on a vector space containing a vector with this cannot be for any norm , since absolute homogeneity would force , which is unbounded in , while is bounded by . So the passage from norms to metrics is not reversible, and a statement about a metric on a vector space is strictly weaker than the corresponding statement about a norm.
Remarks
-
Why (N1) is stated as an equivalence. The direction is forced by (N2) with , since (In any vector space , , , , and forces or ) gives . Only the direction " implies " is a genuine assumption, and dropping it gives what is usually called a seminorm, a notion this library does not use. The analogous weakening in Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric retains symmetry and the triangle inequality but replaces separation by ; that defines a pseudometric.
-
The zero space carries exactly one norm. If then the only function satisfying (N1) is the one with value , and it satisfies (N2) and (N3) trivially. In particular , the function space on the empty index set (The vector space of all functions with pointwise operations, and as the case ), is a normed space, although the metrics of the published metric theory on are defined only for .
-
What is not defined here. This item does not define linear maps; their published definition is Linear map between vector spaces over the same field. It also does not define operator norms, dual spaces, or abstract inner product spaces. Conventions of this page, the standing hypothesis, and what is taken up elsewhere in the reading order records the remaining scope boundaries and what each later development would license.
Depends on
Vector space over a field
The vector space of all functions with pointwise operations, and as the case
Linear map between vector spaces over the same field
Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric
Nonnegativity of a metric is a consequence of the other axioms, not an axiom
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
and are metrics uniformly equivalent to , so every metric space carries a bounded metric with the same topology
Absolute value in an ordered field
Basic properties of the absolute value
The triangle inequality
Complete ordered field (least-upper-bound property)
In any vector space , , , , and forces or