TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedverified 2026-09-26 (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.

Surjectivity is equivalent to a lower bound for the transpose

Statement

Let $K = R$ or $C$ . Assume the Axiom of Choice. For a bounded linear $T : X \to Y$ between Banach spaces, $T is onto ⟺ \exists C > 0 \forall g \in Y^{*} : ∥ g ∥ \leq C ∥ T^{*} g ∥ .$

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.

[F0]

The Axiom of Choice implies dependent choice (AC implies DC implies countable choice).

[F1]

From A lower bound for the transpose forces a dense image of a ball, under the assumed Choice needed by its separation proof: Let $K = R$ or $C$ . 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 ∥} .$

[F2]

From Successive approximation turns a closure-ball inclusion into an actual preimage, with its stated hypotheses: Assume DC. Let $T : X \to Y$ be bounded linear, with $X$ Banach. If $B_{Y} (0, r) \subseteq \overline{T (B_{X} (0, 1))}$ for some $r > 0$ , then $B_{Y} (0, r / 2) \subseteq T (B_{X} (0, 1)) .$

[F3]

From Quantitative lifting form of the open mapping theorem, with its stated hypotheses: Assume DC. For a surjective bounded linear $T : X \to Y$ between Banach spaces, some $c > 0$ satisfies $c B_{Y} (0, 1) \subseteq T (B_{X} (0, 1))$ .

Proof

1.1F3

If $T$ is onto, quantitative open mapping supplies $c > 0$ with $c B_{Y} (0, 1) \subseteq T (B_{X} (0, 1))$ . Taking the supremum of $∣ g ∣$ over these balls gives $c ∥ g ∥ \leq ∥ T^{*} g ∥$ . Hence $C = 1 / c$ works, also for $g = 0$ .

1.2F0F1F2

Conversely the dual estimate yields $B_{Y} (0, 1 / C) \subseteq \overline{T (B_{X} (0, 1))}$ under the assumed Choice. It supplies DC, so successive approximation in the Banach domain gives $B_{Y} (0, 1 / (2 C)) \subseteq T (B_{X} (0, 1))$ .

2.1step 1.2∎

For any nonzero $y \in Y$ , choose the explicit scale $a = 4 C ∥ y ∥ > 0$ . Then $y / a$ lies in that image ball, so multiplying a preimage by $a$ yields a preimage of $y$ . Zero has preimage zero. Thus $T$ is onto, including the case $Y = 0$ .

Remark

The estimate is tested on a given dual input $g$ . The reverse direction then establishes existence of primal solutions; an a priori bound alone must not be described as an already constructed solution.

Depends on

Used by

Banach closed-range theorem Theorem

Dependency tree · two levels

18 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 4.17(i), p.181, with Theorem 4.16 p.180 (standard reference, not scraped)