TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01

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 ( ${A C}_{ω}$ )). Let $X$ be a normed space. The published metric completion of the norm metric on $X$ admits a unique vector-space structure and norm whose induced metric is the published completion metric and such that the constant sequence embedding $i : X \to \hat{X}$ is a dense linear isometry. With this structure, $\hat{X}$ is a Banach space.

Facts & Assumptions

Given: The Axiom of Countable Choice; a normed space $X$ , its published metric completion $\hat{X}$ by Cauchy classes, and the constant-sequence embedding $i : X \to \hat{X}$ .

[A1]

Countable Choice has the meaning fixed in The Axiom of Countable Choice ( ${A C}_{ω}$ ).

[L1]

Under Countable Choice, the published metric completion exists, is complete, and $i [X]$ is dense in it (Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences).

[L2]

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).

[L3]

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).

[L4]

Addition and scalar multiplication are continuous in every normed space (Vector addition and scalar multiplication are continuous in a normed space).

Proof

technique · direct

1.1L2

By [L2], the Cauchy classes carry termwise addition and scalar multiplication, and each class has a well-defined norm $∥ [x_{n}] ∥ : = \lim_{n} ∥ x_{n} ∥$ .

2.1step 1.1L2

On constant sequences these operations agree with those of $X$ , and $∥ i (x) ∥ = ∥ x ∥$ by definition, so $i$ is a linear isometry.

2.2step 1.1L1L2

For classes $[x_{n}]$ and $[y_{n}]$ , the distance of the published metric completion is $\lim_{n} ∥ x_{n} - y_{n} ∥$ , while the new difference class is $[x_{n} - y_{n}]$ ; therefore the completion metric is exactly the metric induced by the norm from step 1.1.

3.1step 2.1step 2.2A1L1L3

By [A1], the underlying metric space is complete by [L1], so step 2.2 makes $\hat{X}$ complete for its new norm metric. Thus $\hat{X}$ is Banach and $(\hat{X}, i)$ is a completion of $X$ in the sense of [L3].

3.2step 2.1L4

Suppose a second Banach-space structure on the same underlying set induces the published completion metric and also makes $i$ 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 $i [X] \times i [X]$ and on $K \times i [X]$ ; therefore they agree everywhere.

4.1step 2.2step 3.2∎

The norm is then forced as well, because in any compatible normed structure $∥ u ∥$ equals the metric distance from $u$ to $0$ . So the compatible Banach-space structure is unique.

The metric completion of a normed space carries a unique compatible Banach-space structure

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources