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:X→Y between Banach spaces, ran⁡T is norm closed⟺∃C>0 ∀x∈X: dist⁡(x,ker⁡T)≤C∥Tx∥.

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 M≤X 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 M≤X be a closed linear subspace, let q:X→X/M be the quotient map, and let T:X→Y be a bounded linear operator with M⊆ker⁡T. Then there is a unique bounded linear operator T‾:X/M→Y such that T‾∘q=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 W⊆V 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:X→Y between Banach spaces has a bounded linear inverse T−1:Y→X.

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

Proof

1.1F2F3

The kernel N=ker⁡T is closed: xj→x 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:Z→Y, A(x+N)=Tx, with range ran⁡T.

2.1F4F5step 1.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+N∥≤C∥Tx∥ with a positive C (enlarge a zero bound if necessary). This is the required distance estimate.

3.1F6step 1.1given∎

Conversely the estimate is ∥z∥≤C∥Az∥ for every z∈Z, 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 0≤0 for any positive C; all steps cover this case.

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