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.
The metric completion of a normed space carries a unique compatible Banach-space structure
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let be a normed space. The published metric completion of the norm metric on admits a unique vector-space structure and norm whose induced metric is the published completion metric and such that the constant sequence embedding is a dense linear isometry. With this structure, is a Banach space.
Facts & Assumptions
Given: The Axiom of Countable Choice; a normed space , its published metric completion by Cauchy classes, and the constant-sequence embedding .
Countable Choice has the meaning fixed in The Axiom of Countable Choice ().
Under Countable Choice, the published metric completion exists, is complete, and is dense in it (Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences).
Termwise addition, scalar multiplication, and the limiting norm on Cauchy classes are well defined (The Cauchy-class operations of a normed-space completion are well defined).
A Banach space is a normed space complete for its norm metric, and a completion of a normed space is a Banach space with dense linear isometry from the original space (Banach space, Completion of a normed space).
Addition and scalar multiplication are continuous in every normed space (Vector addition and scalar multiplication are continuous in a normed space).
Proof
By [L2], the Cauchy classes carry termwise addition and scalar multiplication, and each class has a well-defined norm .
On constant sequences these operations agree with those of , and by definition, so is a linear isometry.
For classes and , the distance of the published metric completion is , while the new difference class is ; therefore the completion metric is exactly the metric induced by the norm from step 1.1.
By [A1], the underlying metric space is complete by [L1], so step 2.2 makes complete for its new norm metric. Thus is Banach and is a completion of in the sense of [L3].
Suppose a second Banach-space structure on the same underlying set induces the published completion metric and also makes a dense linear isometry. Its addition and scalar multiplication are continuous by [L4], and they agree with the operations of step 1.1 on the dense subset and on ; therefore they agree everywhere.
The norm is then forced as well, because in any compatible normed structure equals the metric distance from to . So the compatible Banach-space structure is unique.
Depends on
- Banach space
- Completion of a normed space
- The Cauchy-class operations of a normed-space completion are well defined
- Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences
- Vector addition and scalar multiplication are continuous in a normed space
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- E-valued Dolbeault operators and their L2 structure Definition
- Real-order Bessel-potential completion Hˢ Definition
- Positive type on a discrete group: the identity mass, characters, and the regular GNS model Example
- Bounded linear maps extend uniquely across the completion Theorem
- The norm completion of an inner-product space is a Hilbert space Theorem
Dependency tree · two levels
40 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
- Theo Buhler and Dietmar A. Salamon, Functional Analysis (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)