TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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 Banach space is reflexive if and only if its dual is reflexive

Statement

Assume HB and the Axiom of Countable Choice ${A C}_{ω}$ . A real or complex Banach space $X$ is reflexive if and only if its dual $X^{*}$ is reflexive.

Facts & Assumptions

Given: HB, ${A C}_{ω}$ , and a real or complex Banach space $X$ .

[F1]

A Banach space is reflexive exactly when its canonical map into its bidual is surjective; surjectivity means that every member of the bidual is evaluation at a vector (Reflexivity is surjectivity of the canonical map).

[F2]

Under HB the canonical map $J_{E} : E \to E^{* *}$ of every real or complex normed space is scalar-linear and isometric, hence injective (Relative Hahn–Banach makes the canonical bidual map an isometry).

[F3]

Assuming ${A C}_{ω}$ , a norm-complete subspace of a normed space is closed (A complete normed subspace is closed under countable choice).

[F4]

Under HB, a point outside a nonempty closed convex subset of a real or complex normed space is strictly separated from it by a nonzero bounded scalar-linear functional; the inequalities use its real part (Relative geometric Hahn–Banach with the exact open, closed, and compact hypotheses, part (ii)).

[F5]

HB is the real dominated-extension principle over ZF, and ${A C}_{ω}$ is choice for each supplied sequence of nonempty sets (The real dominated-extension principle as an additional hypothesis over ZF, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct in both directions

1.1

If $X = {0}$ , every scalar-linear functional on $X$ is zero, so $X^{*} = X^{* *} = X^{* * *} = {0}$ and both canonical maps are surjective. The equivalence therefore holds in the zero-space case.

F1algebra

1.2

Suppose first that $X$ is reflexive. Let $Λ \in X^{* * *}$ and define $f = Λ \circ J_{X}$ . Scalar linearity of the two maps makes $f$ scalar-linear, and [F2] gives $∣ f (x) ∣ \leq ∥ Λ ∥ ∥ J_{X} x ∥ = ∥ Λ ∥ ∥ x ∥$ , so $f \in X^{*}$ .

F2given

1.3

Conversely, suppose that $X^{*}$ is reflexive and put $W = J_{X} (X) \subseteq X^{* *}$ . The image $W$ is a scalar-linear subspace by [F2]. It is complete: if $(J_{X} x_{n})$ is Cauchy in its restricted norm, then $∥ x_{n} - x_{m} ∥ = ∥ J_{X} x_{n} - J_{X} x_{m} ∥$ makes $(x_{n})$ Cauchy in the Banach space $X$ ; for its limit $x$ , the same equality gives $J_{X} x_{n} \to J_{X} x$ in $W$ .

F2given

2.1

For arbitrary $x^{* *} \in X^{* *}$ , reflexivity of $X$ supplies an $x \in X$ with $x^{* *} = J_{X} x$ . Then $J_{X^{*}} (f) (x^{* *}) = x^{* *} (f) = J_{X} x (f) = f (x) = Λ (J_{X} x) = Λ (x^{* *})$ . Thus $J_{X^{*}} (f) = Λ$ . Since $Λ$ was arbitrary, $J_{X^{*}}$ is surjective and $X^{*}$ is reflexive. This chooses only one representing vector for one arbitrary $x^{* *}$ at a time.

F1step 1.2

2.2

Apply [F3] under the assumed ${A C}_{ω}$ . The complete subspace $W$ is closed in $X^{* *}$ . It is also nonempty and convex because it is a linear subspace.

F3F5step 1.3

3.1

Suppose for contradiction that some $z \in X^{* *} ∖ W$ exists. By [F4] there is a nonzero $Γ \in X^{* * *}$ that strictly separates the point $z$ from $W$ . In particular, $Re Γ$ is bounded above on $W$ . For $w \in W$ and every real $t$ , also $t w \in W$ ; boundedness of $t Re Γ (w)$ for all $t \in R$ forces $Re Γ (w) = 0$ . In the complex case $i w \in W$ as well, so $0 = Re Γ (i w) = - Im Γ (w)$ ; hence in either field $Γ ∣_{W} = 0$ .

F4step 2.2assume-contraalgebra

4.1

Reflexivity of $X^{*}$ supplies $f \in X^{*}$ with $Γ = J_{X^{*}} (f)$ . For every $x \in X$ , step 3.1 yields $0 = Γ (J_{X} x) = J_{X} x (f) = f (x)$ . Thus $f = 0$ , whence $Γ = J_{X^{*}} (0) = 0$ , contradicting the nonzero separator in step 3.1.

F1step 3.1discharge-contradiction: step 3.1

5.1

No point of $X^{* *}$ lies outside $W$ , so $J_{X} (X) = X^{* *}$ and [F1] says that $X$ is reflexive. This proves the reverse implication and hence the equivalence. HB is used only in the isometry [F2] and separation [F4]; ${A C}_{ω}$ is used only in step 2.2 through [F3].

F1F2F3F4step 4.1∎

Source notes

Bühler–Salamon, Theorem 2.71(i), printed pp. 89–90, supplies the complete canonical-map and annihilator argument. The proof above replaces the source's ordinary-choice background by the repository's exact local bookkeeping: ${A C}_{ω}$ is stated because the selected complete-subspace-closed supplier assumes it, while HB is stated separately for bidual isometry and geometric separation. The complex branch is supplied by the real-part and $i W$ calculation in step 3.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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 (standard reference, not scraped)