Alphabeta Math
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.

A bounded linear map from a dense normed subspace into a Banach space extends uniquely with the same norm

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)).

Let X be a normed space, let DX be a dense normed subspace, let Y be a Banach space, and let T:DY be a bounded linear operator. Then there is a unique bounded linear operator T~:XY such that

T~D=T,

and T~=T.

Facts & Assumptions

Given: The Axiom of Countable Choice, a normed space X, a dense normed subspace DX, a Banach space Y, and a bounded linear operator T:DY.

[L0]

Countable Choice is assumed (The Axiom of Countable Choice (ACω)).

[L1]

A bounded linear operator has a constant C0 with TuCu for all u, and it is continuous (A bounded linear operator between normed spaces, For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent).

[L2]

A Banach space is complete for its norm metric (Banach space).

[L3]

A normed subspace carries the restricted norm, and density means every ball in X meets D (Normed subspace, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[L4]

Limits in a metric space are unique, and addition and scalar multiplication are continuous in normed spaces (A sequence in a metric space has at most one limit, Vector addition and scalar multiplication are continuous in a normed space).

Proof

technique · direct
1.1

Fix xX. By [L0] and density in [L3], for each n1 choose dn(x)D with dn(x)x<1/n. This is the selected ACω step: one approximating sequence for each fixed point x.

L0L3choose
2.1

Let C be a bound for T from [L1]. Then Tdn(x)Tdm(x)Cdn(x)dm(x)C(dn(x)x+dm(x)x), so (Tdn(x)) is Cauchy in Y. By [L2] it converges. Define T~(x):=limnTdn(x).

step 1.1L1L2choose
3.1

The value in step 2.1 is independent of the chosen approximating sequence. If en(x)D also satisfies en(x)x, then Tdn(x)Ten(x)Cdn(x)en(x)C(dn(x)x+en(x)x)0, so the two image sequences have the same limit by [L4].

step 2.1L1L4algebra
3.2

Uniqueness: if S:XY is another bounded linear extension of T, then S is continuous by [L1]. For every xX, the sequence dn(x) of step 1.1 lies in D, so Sdn(x)=Tdn(x)T~(x) by step 2.1 and also Sdn(x)Sx by continuity of S. By [L4], Sx=T~(x). Thus S=T~.

step 1.1step 2.1L1L4
4.1

If xD, choose the constant approximating sequence dn(x)=x. Then step 2.1 gives T~(x)=Tx, so T~ extends T.

step 2.1step 3.1
4.2

To prove linearity, let x,yX and choose the approximating sequences of step 1.1 for them. Then dn(x)+dn(y)x+y and λdn(x)λx by [L4]. Using step 3.1 to replace the chosen sequence at x+y by dn(x)+dn(y), and similarly at λx, we get T~(x+y)=limnT(dn(x)+dn(y))=limn(Tdn(x)+Tdn(y)) and T~(λx)=limnλTdn(x). Continuity of addition and scalar multiplication from [L4] lets the limit pass through, so T~(x+y)=T~(x)+T~(y) and T~(λx)=λT~(x).

step 1.1step 3.1L4construct
5.1

The same bound C works for T~. Indeed, with the sequence of step 1.1, Tdn(x)Cdn(x)C(x+dn(x)x)<C(x+1/n). Given ε>0, choose n large enough that T~(x)Tdn(x)<ε and 1/n<ε/C when C>0; then T~(x)Cx+2ε. Hence T~(x)Cx for all x, so T~ is bounded and T~T. Since T~ agrees with T on D, also TT~. Therefore T~=T.

step 2.1step 4.1L1algebra
6.1

Steps 4.1, 4.2, 5.1, and 4.1 prove that T~ is the unique bounded linear extension of T and that it has the same norm.

step 4.1step 4.2step 5.1step 3.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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