Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-01
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.

Under Dependent Choice, a bounded operator between Banach spaces is bounded below exactly when it is injective with closed range

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

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.

Facts & Assumptions

Given: Banach spaces X and Y, and a bounded linear operator T:X→Y.

[L1]

Being bounded below means that some c>0 satisfies ∥Tx∥≥c∥x∥ for every x∈X (A bounded operator that is bounded below).

[L2]

A Banach space is complete, and a closed subspace of a Banach space is Banach (Banach space, A closed subspace of a Banach space is Banach).

[L3]

In a nonempty complete metric space, a countable union of closed sets with empty interior cannot be the whole space (Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior).

[L4]

A map is injective when equal outputs force equal inputs (Injection, surjection, bijection).

Proof

technique · direct
1.1L1L4

Assume T is bounded below, with constant c>0 from [L1]. If Tx=0, then 0=∥Tx∥≥c∥x∥, so ∥x∥=0 and x=0. Thus T is injective.

1.2L1L2choose

Let (Txn) be a sequence in ran⁡(T) converging to y∈Y. Then ∥xn−xm∥≤c−1∥Txn−Txm∥ by [L1], so (xn) is Cauchy in X and hence converges to some x∈X by [L2]. If C is any bound for T, then ∥Txn−Tx∥≤C∥xn−x∥→0, so Txn→Tx. Since limits are unique in normed spaces, y=Tx. Therefore ran⁡(T) is closed.

1.3L2L4

Conversely, assume T is injective and ran⁡(T) is closed. Then Z:=ran⁡(T) is Banach by [L2], and T:X→Z is a bounded linear bijection.

1.4L0L2L3choose

Let B:={x∈X:∥x∥<1}. Since Z=⋃n≥1T(nB)‾, [L0] and [L3] yield an integer N≥1 such that T(NB)‾ has nonempty interior in Z. So there exist z0∈Z and r>0 with BZ(z0,r)⊆T(NB)‾. Because 0∈T(NB)‾ as well, subtraction gives BZ(0,r)⊆T(2NB)‾.

2.1step 1.4L2chooseconstruct

We claim that every y∈Z with ∥y∥<r has a preimage x with Tx=y and ∥x∥≤4N. Start with e0:=y. If ∥ek∥<r 2−k, then ∥2kek∥<r, so step 1.4 gives vk∈2NB with ∥2kek−Tvk∥<r/2. Put uk:=2−kvk and ek+1:=ek−Tuk. Then ∥uk∥≤2N 2−k and ∥ek+1∥<r 2−k−1. Inductively this constructs (uk) with ∥ek∥<r 2−k for every k. The series ∑kuk is absolutely convergent because ∑k2N 2−k<∞, so [L2] gives x:=∑kuk∈X with ∥x∥≤4N. Also y−T(∑j<muj)=em→0, hence Tx=y.

3.1step 2.1algebra

Now let z∈Z with z≠0. Put λ:=r/(2∥z∥), so ∥λz∥=r/2<r. Step 2.1 gives u∈X with Tu=λz and ∥u∥≤4N. Then x:=λ−1u satisfies Tx=z and ∥x∥≤(8N/r)∥z∥. The same inequality is trivial at z=0, so the inverse T−1:Z→X is bounded by 8N/r.

4.1step 3.1L1

Applying step 3.1 to z=Tx gives ∥x∥≤(8N/r)∥Tx∥ for every x∈X, that is, ∥Tx∥≥(r/8N)∥x∥. Therefore T is bounded below.

5.1step 1.1step 1.2step 1.3step 4.1∎

Step 1.2 proves that bounded below implies injective with closed range, and steps 1.3 through 4.1 prove the converse.

Depends on

Used by

Dependency tree · two levels

24 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