Alphabeta Math
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.

Closed range is equivalent to a quotient estimate

Statement

Let K=R or C. Assume DC. For a bounded linear map T:XY between Banach spaces, ranT is norm closedC>0 xX: dist(x,kerT)CTx.

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.

[F2]

From A quotient of a Banach space by a closed subspace is Banach, with its stated hypotheses: Assume the Axiom of Countable Choice (def-countable-choice). Let X be a Banach space and let MX be a closed linear subspace. Then X/M is Banach for the quotient norm.

[F3]

From A bounded operator that vanishes on a subspace factors uniquely through the normed quotient, with its stated hypotheses: Let X and Y be normed spaces over the same scalar field, let MX be a closed linear subspace, let q:XX/M be the quotient map, and let T:XY be a bounded linear operator with MkerT. Then there is a unique bounded linear operator T:X/MY such that Tq=T, and moreover T=T.

[F4]

From A closed subspace of a Banach space is Banach, with its stated hypotheses: Let V be a Banach space and let WV be a closed linear subspace, equipped with the restricted norm. Then W is a Banach space.

[F5]

From Bounded inverse theorem, with its stated hypotheses: Assume DC. A bounded bijective linear map T:XY between Banach spaces has a bounded linear inverse T1:YX.

[F6]

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:XY be a bounded linear operator. Then T is bounded below if and only if it is injective and has closed range.

Proof

1.1

The kernel N=kerT is closed: xjx with Txj=0 implies Tx=0 by boundedness. DC supplies the countable choice required for quotient completeness, so Z=X/N is Banach. The quotient universal property gives a bounded injective A:ZY, A(x+N)=Tx, with range ranT.

F2F3
2.1

If that range is closed, it is Banach. View A as a bounded bijection onto this range and use bounded inverse to obtain x+NCTx with a positive C (enlarge a zero bound if necessary). This is the required distance estimate.

F4F5step 1.1
3.1

Conversely the estimate is zCAz for every zZ, so A is bounded below. Since Z and Y are Banach, the bounded-below criterion makes its range closed. If T=0, then Z=0 and the estimate is 00 for any positive C; all steps cover this case.

F6step 1.1given

Depends on

Used by

Dependency tree · two levels

25 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