LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

A compact remainder estimate forces 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$ , $Y$ and $Z$ be Banach spaces over the same scalar field, let $T : X \to Y$ and $K : X \to Z$ be bounded linear operators with $K$ compact (A bounded linear operator between normed spaces, Compact linear operator), and suppose there is a real $C > 0$ with

$∥ x ∥ \leq C ∥ T x ∥ + ∥ K x ∥ for every x \in X .$

Then $\ker T$ is finite dimensional and $ran T$ is closed in $Y$ .

Facts & Assumptions

[A1]

Bounded linear operators are continuous, and the kernel of $T$ is a closed subspace of $X$ (For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent, A bounded linear operator between normed spaces); limits of sequences in a metric space are unique (A sequence in a metric space has at most one limit, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[A2]

Assume DC. Then Countable Choice holds (Dependent choice implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )); a compact operator maps bounded sequences to sequences with convergent subsequences (Sequential characterization of compact operators, Sequences of reals: bounded, eventually, frequently, tails, subsequences, A strictly increasing index map satisfies $n_{k} \geq k$ ); a normed space with compact closed unit ball admits an ordered basis of finite length (The closed unit ball is compact if and only if the normed space is finite-dimensional); compact, sequentially compact and complete-and-totally-bounded agree for metric spaces under ${A C}_{ω}$ and DC (For a metric space, compact, countably compact, limit point compact, sequentially compact, and complete together with totally bounded are all equivalent, given countable choice and dependent choice).

[A3]

Under DC, $ran T$ is closed exactly when there is a real $C^{'} > 0$ with $dist (x, \ker T) \leq C^{'} ∥ T x ∥$ for every $x$ (Closed range is equivalent to a quotient estimate, The quotient seminorm (|x+M|{X/M}=\inf{m\in M}|x+m|=\operatorname{dist}(x,M))); the distance scales, $dist (λ x, \ker T) = ∣ λ ∣ dist (x, \ker T)$ , because $\ker T$ is a subspace, and $dist (u, M) \leq ∥ u ∥$ for nonempty $M ∋ 0$ .

[A4]

If $(u_{j})$ is Cauchy and some subsequence converges to $u$ , then $u_{j} \to u$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ); a closed set contains the limits of its convergent sequences (Banach space, A sequence in a metric space has at most one limit).

Proof

technique · direct

Given: $D C$ , Banach spaces $X, Y, Z$ over one scalar field, bounded $T : X \to Y$ , compact $K : X \to Z$ , a real $C > 0$ with $∥ x ∥ \leq C ∥ T x ∥ + ∥ K x ∥$ for all $x$ , and $N : = \ker T$ .

1.1

For $x \in N$ the estimate reads $∥ x ∥ \leq ∥ K x ∥$ , so $∥ K x - K x^{'} ∥ = ∥ K (x - x^{'}) ∥ \geq ∥ x - x^{'} ∥$ for all $x, x^{'} \in N$ .

algebra

1.2

The set $N$ is a closed subspace, hence a Banach space.

A1A4

1.3

For every real $η > 0$ there is $x$ with $dist (x, N) = 1$ , $∥ x ∥ \leq 2$ and $∥ T x ∥ < η$ whenever the estimate of [A3] fails for every constant: failure for the constant $C^{'} = 1 / η$ gives $x_{0}$ with $dist (x_{0}, N) > ∥ T x_{0} ∥ / η \geq 0$ and $dist (x_{0}, N) > 0$ , and choosing $m \in N$ with $∥ x_{0} - m ∥ < 2 dist (x_{0}, N)$ and setting $x : = (x_{0} - m) / dist (x_{0}, N)$ gives the three properties by scaling.

A3algebra

2.1

The closed unit ball $B_{N} : = N \cap {x : ∥ x ∥ \leq 1}$ is compact: if $(x_{j})$ is a sequence in $B_{N}$ , then it is bounded so by [A2] some subsequence has $K x_{j_{k}} \to z$ ; by [step 1.1] the subsequence is Cauchy, $∥ x_{j_{k}} - x_{j_{l}} ∥ \leq ∥ K x_{j_{k}} - K x_{j_{l}} ∥$ , hence converges to some $x \in N$ by [step 1.2], and $∥ x ∥ \leq 1$ ; thus every sequence in $B_{N}$ has a subsequence converging in $B_{N}$ , so $B_{N}$ is sequentially compact, hence compact by [A2].

step 1.1step 1.2A2

2.2

If the estimate of [A3] fails for every constant, then [step 1.3] makes the set of witnesses with $dist (w, N) = 1$ , $∥ w ∥ \leq 2$ and $∥ T w ∥ < 1 / (j + 1)$ nonempty for each $j$ ; Countable Choice in [A2] therefore supplies a sequence $(w_{j})$ with those three properties.

step 1.3A2

3.1

$\ker T$ is finite dimensional: its closed unit ball is compact by [step 2.1], so $N$ admits an ordered basis of finite length by [A2].

step 2.1A2

3.2

Under the hypothesis of [step 2.2] the bounded sequence $(w_{j})$ has, by [A2], a subsequence with $K w_{j_{k}} \to z$ for some $z \in Z$ .

step 2.2A2

4.1

Under the hypothesis of [step 2.2], the subsequence is Cauchy: $∥ w_{j_{k}} - w_{j_{l}} ∥ \leq C ∥ T (w_{j_{k}} - w_{j_{l}}) ∥ + ∥ K (w_{j_{k}} - w_{j_{l}}) ∥ \leq C (1 / (j_{k} + 1) + 1 / (j_{l} + 1)) + ∥ K w_{j_{k}} - K w_{j_{l}} ∥$ , and both terms tend to $0$ ; hence $w_{j_{k}} \to w$ for some $w \in X$ .

step 2.2step 3.2A4algebra

5.1

Under the hypothesis of [step 2.2], the limit $w$ lies in $N$ : $T w = \lim_{k} T w_{j_{k}} = 0$ by the continuity of $T$ and $∥ T w_{j_{k}} ∥ < 1 / (j_{k} + 1)$ .

step 2.2step 4.1A1A4

6.1

Under the hypothesis of [step 2.2], the numbers $dist (w_{j_{k}}, N) = 1$ converge to $dist (w, N)$ because the distance to a fixed set is 1-Lipschitz, so $dist (w, N) = 1$ , contradicting $w \in N$ of [step 5.1], which forces $dist (w, N) = 0$ .

step 2.2step 4.1step 5.1A3

7.1

Hence the estimate of [A3] holds for some constant, and then $ran T$ is closed by [A3]; together with [step 3.1] this proves the lemma.

step 3.1step 6.1A3∎

Depends on

Used by

Atkinson Theorem

Dependency tree · two levels

85 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

Theo Bühler and Dietmar Salamon, Functional Analysis — §4.3 pp.193–194, Lemma 4.39 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §6.5, closed range from a compact remainder (standard reference, not scraped)