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.

Range of identity minus compact is closed

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$ be a Banach space over $R$ or $C$ , let $K : X \to X$ be a compact operator (Compact linear operator) and put $A : = I - K$ . Then $ran A$ is a closed subspace of $X$ , and there is a real $C > 0$ with

$dist (x, \ker A) \leq C ∥ A x ∥ for every x \in X,$

the distance being the quotient seminorm of The quotient seminorm (|x+M|{X/M}=\inf{m\in M}|x+m|=\operatorname{dist}(x,M)).

Facts & Assumptions

[A1]

$ran A$ is closed if and only if there is a real $C > 0$ with $dist (x, \ker A) \leq C ∥ A x ∥$ for every $x$ , under DC for the bounded linear map $A$ between Banach spaces (Closed range is equivalent to a quotient estimate); here $dist (x, M) = ∥ x + M ∥_{X / M}$ is the quotient seminorm (The quotient seminorm (|x+M|{X/M}=\inf{m\in M}|x+m|=\operatorname{dist}(x,M))).

[A2]

$K$ is bounded and bounded linear operators are continuous (A bounded linear operator between normed spaces, For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent); DC implies Countable Choice (Dependent choice implies countable choice), and under DC 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$ ).

[A3]

In a metric space, limits of sequences 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$ ); the distance to a fixed set is 1-Lipschitz, $∣ dist (u, N) - dist (v, N) ∣ \leq ∥ u - v ∥$ (The quotient seminorm (|x+M|{X/M}=\inf{m\in M}|x+m|=\operatorname{dist}(x,M))).

Proof

technique · direct

Given: $D C$ , a Banach space $X$ over $R$ or $C$ , a compact operator $K : X \to X$ , and $A = I - K$ , $N : = \ker A$ .

1.1

$N$ is a closed linear subspace: $A$ is bounded hence continuous by [A2], so $x_{j} \in N$ with $x_{j} \to x$ gives $A x_{j} = 0 \to A x$ , whence $A x = 0$ by [A3].

A2A3

1.2

If the estimate of [A1] fails for every $C$ , then for each fixed $n \in N$ the set $W_{n} : = {w : dist (w, N) = 1, ∥ w ∥ \leq 2, ∥ A w ∥ < 1 / (n + 1)}$ is nonempty: taking $C = n + 1$ gives $x$ with $dist (x, N) > (n + 1) ∥ A x ∥ \geq 0$ , so the distance is positive; choose $m \in N$ with $∥ x - m ∥ < 2 dist (x, N)$ by the definition of the infimum, and set $w : = (x - m) / dist (x, N)$ . Scaling the distance gives $dist (w, N) = 1$ , the norm bound $∥ w ∥ < 2$ holds, and $∥ A w ∥ = ∥ A x ∥ / dist (x, N) < 1 / (n + 1)$ because $A m = 0$ .

step 1.1A1A3algebra

2.1

Assume the estimate fails. By Countable Choice in [A2], select $w_{n} \in W_{n}$ for every $n$ as in [step 1.2], and put $M : = {x \in X : ∥ x ∥ \leq 2}$ . The sequence $(w_{n})$ lies in the bounded set $M$ , and $K$ is compact, so by [A2] there is a strictly increasing $j$ with $K w_{n_{j}} \to z$ for some $z \in X$ .

step 1.2A2

3.1

Along that subsequence, $w_{n_{j}} = A w_{n_{j}} + K w_{n_{j}} \to z$ , because $∥ A w_{n_{j}} ∥ < 1 / (n_{j} + 1) \to 0$ by [step 1.2] and $K w_{n_{j}} \to z$ by [step 2.1].

step 1.2step 2.1algebra

4.1

The limit $z$ lies in $N$ : by [step 3.1] and the continuity of $A$ , $A z = \lim_{j} A w_{n_{j}} = 0$ .

step 3.1A2A3

5.1

But this contradicts $dist (w_{n_{j}}, N) = 1$ : by [A3] the numbers $dist (w_{n_{j}}, N)$ converge to $dist (z, N)$ , so $dist (z, N) = 1$ , whereas $z \in N$ forces $dist (z, N) = 0$ .

step 1.2step 3.1step 4.1A3

6.1

Hence the estimate of [A1] holds for some real $C > 0$ , and then [A1] gives that $ran A$ is closed.

step 5.1A1∎

Depends on

Used by

Dependency tree · two levels

71 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, Lemma 4.39 (closed range of I minus compact) (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §6.5, Riesz–Schauder theory (standard reference, not scraped)