Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generated
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 functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed

Statement

Assume the Axiom of Choice. Let X be a normed space over R or C, let M⊆X be a linear subspace, and let f0:M→R or f0:M→C be a bounded linear functional over the ambient scalar field. Then there exists a bounded linear extension F of f0 to all of X such that ∥F∥=∥f0∥.

No closedness hypothesis on M is needed.

Facts & Assumptions

Given: The Axiom of Choice, A normed space X over R or C, a linear subspace M⊆X, and a bounded linear functional f0 on M.

[A1]

AC is used through [L1] or [L2] in steps 1.1 and 1.2.

[L1]

In the real case, a bounded linear functional on a subspace extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).

[L2]

In the complex case, a bounded linear functional on a subspace extends with the same norm (A bounded complex linear functional on a subspace of a complex normed space extends with the same norm).

Proof

technique · direct
1.1L1L3given

If the scalar field is R, then [L1] applies exactly as stated to the given subspace M and produces a norm-preserving extension of f0 to X.

1.2L2L3given

If the scalar field is C, then [L2] applies exactly as stated to the given subspace M and produces a norm-preserving extension of f0 to X.

2.1step 1.1step 1.2L1L2∎

Neither step 1.1 nor step 1.2 uses or requires that M be closed; each cited theorem assumes only that M is a linear subspace. Therefore every bounded linear functional on an arbitrary subspace extends with the same norm.

Depends on

Used by

Dependency tree · two levels

28 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