TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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 dual of a closed subspace is a dual quotient

Statement

Let $K = R$ or $C$ . Let $X$ be normed and $M \leq X$ closed. Restriction $R : X^{*} \to M^{*}$ induces a linear isometric bijection $\tilde{R} : X^{*} / M^{⊥} ⟶ M^{*}, f + M^{⊥} ⟼ f ∣_{M} .$ Also $∥ R ∥ \leq 1$ ; its norm is $1$ when $M \neq {0}$ and $0$ when $M = {0}$ .

Facts & Assumptions

Given: The spaces, maps, scalar field, and hypotheses in the statement above. All duals consist of linear functionals over the ambient field; evaluation has no conjugation.

[F1]

From Annihilator notation and the preannihilator, with its stated hypotheses: Let $K = R$ or $C$ . For a normed $X$ and arbitrary subsets $M \subseteq X$ , $N \subseteq X^{*}$ , define $M^{⊥} = {f \in X^{*} : f (m) = 0 for all m \in M},^{⊥} N = {x \in X : f (x) = 0 for all f \in N} .$ Here $X^{*}$ is def-dual-space-of-a-normed-space. The first notation agrees with def-continuous-annihilator-of-a-subspace on $span M$ , since linearity makes vanishing on $M$ equivalent to vanishing on its span. The preannihilator lies in $X$ , not in $X^{* *}$ . Empty sets impose no conditions: $\emptyset^{⊥} = X^{*}$ and $^{⊥} \emptyset = X$ .

[F2]

From Annihilators and preannihilators are norm closed, with its stated hypotheses: Let $K = R$ or $C$ . For any normed $X$ and arbitrary $M \subseteq X$ , $N \subseteq X^{*}$ , both $M^{⊥} \subseteq X^{*}$ and $^{⊥} N \subseteq X$ are norm-closed linear subspaces. Moreover ${\overline{N}}^{∥ \cdot ∥} \subseteq (^{⊥} N)^{⊥}$ .

[F3]

From A bounded operator that vanishes on a subspace factors uniquely through the normed quotient, with its stated hypotheses: Let $X$ and $Y$ be normed spaces over the same scalar field, let $M \leq X$ be a closed linear subspace, let $q : X \to X / M$ be the quotient map, and let $T : X \to Y$ be a bounded linear operator with $M \subseteq \ker T$ . Then there is a unique bounded linear operator $\overline{T} : X / M \to Y$ such that $\overline{T} \circ q = T,$ and moreover $∥ \overline{T} ∥ = ∥ T ∥$ .

[F4]

From A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed, with its stated hypotheses: Let $X$ be a normed space over $R$ or $C$ , let $M \subseteq X$ be a linear subspace, and let $f_{0} : M \to R$ or $f_{0} : M \to C$ be a bounded linear functional over the ambient scalar field. Then there exists a bounded linear extension $F$ of $f_{0}$ to all of $X$ such that $∥ F ∥ = ∥ f_{0} ∥$ . No closedness hypothesis on $M$ is needed.

Proof

1.1

The inequality $∥ f ∣_{M} ∥ \leq ∥ f ∥$ makes restriction bounded. Its kernel is $M^{⊥}$ , which is closed. Thus equal cosets have equal restrictions, and the quotient universal property gives a bounded linear induced map; the kernel calculation makes it injective.

F1F2F3

2.1

For $h \in M^{*}$ , norm-preserving extension gives $f \in X^{*}$ with $f ∣_{M} = h$ and $∥ f ∥ = ∥ h ∥$ , proving surjectivity. Every other representative $f + a$ , $a \in M^{⊥}$ , restricts to $h$ , so $∥ f + a ∥ \geq ∥ h ∥$ . Taking the infimum and using this extension proves $∥ f + M^{⊥} ∥ = ∥ h ∥$ .

F4step 1.1

3.1

If $M \neq {0}$ , fix $m \in M ∖ {0}$ . The functional $λ m \mapsto λ ∥ m ∥$ on its line has norm one. Extend first to $M$ and then to $X$ by norm-preserving extension; its restriction and extension both have norm one, so $∥ R ∥ \geq 1$ . If $M = {0}$ , $R = 0$ . For $M = X$ the induced map is the identity, including the zero ambient space.

F4step 1.1step 2.1∎

Depends on

Used by

Distance to an annihilator is the restriction norm Corollary
Banach closed-range theorem Theorem

Dependency tree · two levels

14 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

Bühler–Salamon, Functional Analysis, Corollary 2.57(i), pp.84–85 (standard reference, not scraped)