LemmaStatement: 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.

Finite evaluations separate a functional from a dual subspace

Statement

Let $K = R$ or $C$ . Let $X$ be normed, $N \leq X^{*}$ a linear subspace, and $x_{1}, \dots, x_{n} \in X$ with $n \geq 1$ . Define $E (f) = (f (x_{1}), \dots, f (x_{n}))$ . If $f_{0} \in X^{*}$ satisfies $E (f_{0}) \notin E (N)$ , there is $x \in span {x_{1}, \dots, x_{n}}$ such that $g (x) = 0$ for all $g \in N$ and $f_{0} (x) = 1$ .

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 A finite-dimensional normed subspace is closed, with its stated hypotheses: Let $V$ be a normed space and let $W \subseteq V$ be a normed subspace. If $W$ admits an ordered basis of finite length, then $W$ is closed in $V$ .

[F3]

From Geometric Hahn--Banach theorem for subspaces, with its stated hypotheses: For a linear subspace $M \subseteq X$ and $x \notin \overline{M}$ , there is $f \in M^{⊥}$ with $f (x) = 1$ .

Proof

1.1

The image $E (N)$ is a linear subspace of the finite-dimensional normed space $K^{n}$ , hence admits a finite basis and is closed. Geometric Hahn–Banach applied to $E (f_{0}) \notin E (N)$ supplies a linear functional $h$ on $K^{n}$ with $h ∣_{E (N)} = 0$ and $h (E (f_{0})) = 1$ .

F2F3

2.1

For the standard coordinate vectors $e_{j}$ , set $a_{j} = h (e_{j})$ and $x = \sum_{j = 1}^{n} a_{j} x_{j}$ . Expanding in that basis gives $h (E (f)) = \sum_{j} a_{j} f (x_{j}) = f (x)$ for every $f \in X^{*}$ . Thus $g (x) = 0$ for $g \in N$ and $f_{0} (x) = 1$ ; in particular $x \in^{⊥} N$ .

F1step 1.1

3.1

Linear dependence among the $x_{j}$ , or $E (N) = 0$ , does not affect either step. For $n = 1$ the same sum has one term. The hypothesis excludes $f_{0} = 0$ and excludes all $x_{j}$ being zero; the conclusion never demands $f_{0} (0) = 1$ .

step 1.1step 2.1∎

Depends on

Used by

Double annihilators give norm and weak-star closures Theorem

Dependency tree · two levels

10 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, Theorem 3.12(ii), pp.125–127, and Corollary 3.26(i), p.130; finite-coordinate adaptation using Theorem 2.53, pp.82–83 (standard reference, not scraped)