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 ()).
Let be a normed space, let be a dense normed subspace, let be a Banach space, and let be a bounded linear operator. Then there is a unique bounded linear operator such that
and .
Facts & Assumptions
Given: The Axiom of Countable Choice, a normed space , a dense normed subspace , a Banach space , and a bounded linear operator .
Countable Choice is assumed (The Axiom of Countable Choice ()).
A bounded linear operator has a constant with for all , 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).
A Banach space is complete for its norm metric (Banach space).
A normed subspace carries the restricted norm, and density means every ball in meets (Normed subspace, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).
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
Fix . By [L0] and density in [L3], for each choose with . This is the selected step: one approximating sequence for each fixed point .
Let be a bound for from [L1]. Then , so is Cauchy in . By [L2] it converges. Define .
The value in step 2.1 is independent of the chosen approximating sequence. If also satisfies , then , so the two image sequences have the same limit by [L4].
Uniqueness: if is another bounded linear extension of , then is continuous by [L1]. For every , the sequence of step 1.1 lies in , so by step 2.1 and also by continuity of . By [L4], . Thus .
If , choose the constant approximating sequence . Then step 2.1 gives , so extends .
To prove linearity, let and choose the approximating sequences of step 1.1 for them. Then and by [L4]. Using step 3.1 to replace the chosen sequence at by , and similarly at , we get and . Continuity of addition and scalar multiplication from [L4] lets the limit pass through, so and .
The same bound works for . Indeed, with the sequence of step 1.1, . Given , choose large enough that and when ; then . Hence for all , so is bounded and . Since agrees with on , also . Therefore .
Steps 4.1, 4.2, 5.1, and 4.1 prove that is the unique bounded linear extension of and that it has the same norm.
Depends on
- A bounded linear operator between normed spaces
- Banach space
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Normed subspace
- A sequence in a metric space has at most one limit
- Vector addition and scalar multiplication are continuous in a normed space
- For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent
- Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
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
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)
- Theo Buhler and Dietmar A. Salamon, Functional Analysis (standard reference, not scraped)