LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-09-23 (gpt-6-sol)

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 lower bound for the transpose forces a dense image of a ball

Statement

Let $K = R$ or $C$ . Assume the Axiom of Choice. Let $T : X \to Y$ be bounded linear between normed spaces, and let $C > 0$ satisfy $∥ g ∥ \leq C ∥ T^{*} g ∥$ for every $g \in Y^{*}$ . With open balls, $B_{Y} (0, 1 / C) \subseteq {\overline{T (B_{X} (0, 1))}}^{∥ \cdot ∥} .$

Facts & Assumptions

Given: The Axiom of Choice and 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 The transpose of a bounded operator, with its stated hypotheses: Let $K = R$ or $C$ . Let $T : X \to Y$ be bounded and linear between normed spaces. Its transpose, or Banach adjoint, is $T^{*} : Y^{*} ⟶ X^{*}, (T^{*} g) (x) = g (T x) .$ The duals are def-dual-space-of-a-normed-space. Composition is bounded by lem-composition-operator-norm-inequality, so this has the displayed codomain. It is linear in $g$ over $K$ . No complex conjugation is inserted; a Hilbert adjoint uses a separate inner-product identification.

[F2]

From The transpose is bounded with the same norm, with its stated hypotheses: Let $K = R$ or $C$ . For a bounded linear $T : X \to Y$ between normed spaces, $T^{*} : Y^{*} \to X^{*}$ is bounded linear and $∥ T^{*} ∥ = ∥ T ∥$ .

[F3]

From Strong separation of a closed and a compact convex set, with its stated hypotheses: under AC, disjoint nonempty convex $C, K \subseteq X$ with $C$ closed and $K$ compact are strongly separated by a nonzero functional in $X^{*}$ .

[A1]

The Axiom of Choice is used exactly when applying [F3] in step 2.1.

Proof

1.1F1F2

Put $D = \overline{T (B_{X} (0, 1))}$ . It contains zero and is closed, convex and balanced: the image ball has these last two algebraic properties, and continuity of linear combinations preserves them on taking closure. For $g \in Y^{*}$ , continuity and phase rotation in the unit ball give $\sup_{y \in D} Re g (y) = \sup_{∥ x ∥ < 1} ∣ g (T x) ∣ = ∥ T^{*} g ∥$ . The open-ball supremum equals the closed-ball supremum by scaling vectors by real numbers tending to one.

2.1F3A1step 1.1given

If $y \notin D$ , [F3] under [A1] strongly separates the nonempty closed convex set $D$ and compact singleton ${y}$ by a nonzero $g \in Y^{*}$ , oriented so that $Re g (y) > \sup_{D} Re g$ . Thus $∥ g ∥ ∥ y ∥ \geq Re g (y) > ∥ T^{*} g ∥ \geq ∥ g ∥ / C$ , hence $∥ y ∥ > 1 / C$ .

3.1step 1.1step 2.1∎

Consequently every point of norm less than $1 / C$ lies in $D$ . Zero was already in $D$ . If $T = 0$ , the hypothesis forces $Y^{*} = 0$ ; separation in step 2.1 rules out any point outside $D = {0}$ , so the argument remains valid even in that degenerate case.

Depends on

Used by

Surjectivity is equivalent to a lower bound for the transpose Theorem

Dependency tree · two levels

13 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 4.16 proof (vii) => (i), (4.10)–(4.11), p.180 (standard reference, not scraped)