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.

Bounded below is equivalent to surjectivity of the transpose

Statement

Let $K = R$ or $C$ . Assume DC. If $T : X \to Y$ is bounded linear between Banach spaces, then $(\exists c > 0 \forall x \in X : ∥ T x ∥ \geq c ∥ x ∥) ⟺ T^{*} : Y^{*} \to X^{*} is onto .$

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 Banach closed-range theorem, with its stated hypotheses: Let $K = R$ or $C$ . Assume DC and let $T : X \to Y$ be bounded linear between Banach spaces. The following are equivalent: $ran T$ is norm closed; $ran T^{*}$ is norm closed; and there is $C > 0$ such that $dist (x, \ker T) \leq C ∥ T x ∥$ for all $x \in X$ . In that case $ran T =^{⊥} (\ker T^{*}), ran T^{*} = (\ker T)^{⊥} .$

[F2]

From Elementary kernel and range annihilator identities, with its stated hypotheses: Let $K = R$ or $C$ . For a bounded linear $T : X \to Y$ between normed spaces, $(ran T)^{⊥} = \ker T^{*},^{⊥} (ran T^{*}) = \ker T, {\overline{ran T}}^{∥ \cdot ∥} =^{⊥} (\ker T^{*}) .$ The closure in the last identity is in $Y$ .

[F3]

From Membership in the transpose range by an operator estimate, with its stated hypotheses: Let $K = R$ or $C$ . Let $T : X \to Y$ be bounded linear between normed spaces and $f \in X^{*}$ . Then $f \in ran T^{*} ⟺ \exists C \geq 0 \forall x \in X : ∣ f (x) ∣ \leq C ∥ T x ∥ .$ For any such $C$ , a representing $g \in Y^{*}$ can be chosen with $∥ g ∥ \leq C$ .

[F4]

From Under Dependent Choice, a bounded operator between Banach spaces is bounded below exactly when it is injective with closed range, with its stated hypotheses: Assume the Axiom of Dependent Choice (def-dependent-choice). Let $X$ and $Y$ be Banach spaces over the same scalar field, and let $T : X \to Y$ be a bounded linear operator. Then $T$ is bounded below if and only if it is injective and has closed range.

Proof

1.1

If $T$ is bounded below with constant $c > 0$ , every $f \in X^{*}$ satisfies $∣ f (x) ∣ \leq ∥ f ∥ ∥ x ∥ \leq (∥ f ∥ / c) ∥ T x ∥$ . Domination gives $f \in ran T^{*}$ , proving surjectivity.

1.2

If $T^{*}$ is onto, its range $X^{*}$ is closed. Closed range duality makes $ran T$ closed. Also $\ker T =^{⊥} X^{*} = {0}$ : the elementary identity applied to the identity operator on $X$ gives the last equality. Thus $T$ is injective with closed range, and the Banach bounded-below criterion applies.

F1F2F4

2.1

When $X = 0$ , the lower bound holds for any positive $c$ and $T^{*}$ maps onto $X^{*} = 0$ . The preceding arguments cover this case without choosing a unit vector or dividing by its norm.

step 1.1step 1.2∎

Depends on

Used by

Invertibility and the inverse of the transpose Corollary

Dependency tree · two levels

22 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(ii), p.181 (standard reference, not scraped)