TheoremStatement: 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.

Sequential characterization of compact operators

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 normed spaces over the same scalar field (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, Real and complex scalar conventions for normed spaces) and let $T : X \to Y$ be a bounded linear operator (A bounded linear operator between normed spaces). Then $T$ is compact (Compact linear operator) if and only if every bounded sequence $(x_{k})$ in $X$ , that is every function $x : N \to X$ with bounded range (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space), has a subsequence $(x_{k_{j}})$ , the index map being strictly increasing (Countably compact, sequentially compact and limit point compact metric spaces, A strictly increasing index map satisfies $n_{k} \geq k$ ), for which $(T x_{k_{j}})$ converges in the norm metric of $Y$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

Facts & Assumptions

[A1]

$T$ is compact exactly when $\overline{T ({\overline{B}}_{X})}$ is a compact subset of $Y$ , where ${\overline{B}}_{X} = {x \in X : ∥ x ∥ \leq 1}$ (Compact linear operator).

[A2]

Assume ${A C}_{ω}$ and $D C$ . For a metric space $(M, d)$ , compactness, countable compactness, limit point compactness, sequential compactness and "complete and totally bounded" are equivalent; only "sequentially compact implies totally bounded" spends DC and only "complete and totally bounded implies compact" spends ${A C}_{ω}$ , so every other implication is a theorem of ZF (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]

In ZF, $D C$ implies ${A C}_{ω}$ (Dependent choice implies countable choice); and $D C$ is the statement that for every nonempty set $X$ , every relation $R$ on $X$ entire on $X$ and every $a \in X$ there is $x : N \to X$ with $x_{0} = a$ and $x_{n} R x_{n + 1}$ for all $n$ (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[A4]

A subset $A$ of a metric space is bounded when $A = \emptyset$ or $A \subseteq B (x_{0}, r)$ for some point $x_{0}$ and real $r > 0$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space).

[A5]

In a normed space, $∥ x ∥ \leq R$ implies $x \in R {\overline{B}}_{X}$ ; convergence is metric convergence for $d (y, y^{'}) = ∥ y - y^{'} ∥$ ; a set $F \subseteq Y$ is closed exactly when $F = \overline{F}$ ; for nonempty $A$ the closure is $\overline{A} = {y : d (y, A) = 0}$ ; and the closure of $A$ is contained in every closed set containing $A$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset).

Proof

technique · direct

Given: $D C$ , normed spaces $X, Y$ over one scalar field, a bounded linear $T : X \to Y$ , and the notation ${\overline{B}}_{X} = {x : ∥ x ∥ \leq 1}$ .

1.1

Suppose $T$ compact and let $(x_{k})$ be a bounded sequence in $X$ . By [A4] the range ${x_{k}}$ is empty or contained in some ball $B (x_{0}, r)$ ; because $∥ x_{k} ∥ \leq ∥ x_{k} - x_{0} ∥ + ∥ x_{0} ∥$ for every $k$ , there is a real $R \geq 0$ with $∥ x_{k} ∥ \leq R$ for all $k$ (if the range is empty take $R = 0$ ), and then $T x_{k} \in R \overline{T ({\overline{B}}_{X})}$ for every $k$ , because $x_{k} \in R {\overline{B}}_{X}$ and $T$ is linear.

A4A5algebra

1.2

Conversely assume every bounded sequence in $X$ has a subsequence whose $T$ -images converge, and put $C : = \overline{T ({\overline{B}}_{X})}$ . Let $(y_{k})$ be a sequence in $C$ . For each $k$ the set $S_{k} : = {x \in {\overline{B}}_{X} : ∥ y_{k} - T x ∥ < 1 / (k + 1)}$ is nonempty, because $y_{k} \in \overline{T ({\overline{B}}_{X})}$ , the set $T ({\overline{B}}_{X})$ is nonempty, and [A5] then gives a point of $T ({\overline{B}}_{X})$ within $1 / (k + 1)$ of $y_{k}$ ; selecting $x_{k} \in S_{k}$ for every $k$ is a countable selection from nonempty sets, which [A3] licenses.

A3A5

2.1

By [A1] the set $\overline{T ({\overline{B}}_{X})}$ is compact, and multiplication by the scalar $R$ is continuous, so $R \overline{T ({\overline{B}}_{X})}$ is a compact subset of $Y$ (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism); by [A2] its metric subspace is sequentially compact, so the sequence $(T x_{k})$ of [step 1.1] has a subsequence converging in $Y$ .

step 1.1A1A2

2.2

The sequence $(x_{k})$ of [step 1.2] is bounded, since its range lies in ${\overline{B}}_{X}$ ; by hypothesis some subsequence $(x_{k_{j}})$ has $T x_{k_{j}} \to y$ for some $y \in Y$ , and since every $T x_{k_{j}}$ lies in $T ({\overline{B}}_{X}) \subseteq C$ while $C$ is closed, [A5] gives $y \in C$ .

step 1.2A4A5

3.1

Therefore compactness of $T$ implies the stated sequential property for every bounded sequence.

step 2.1

3.2

Along that subsequence $∥ y_{k_{j}} - y ∥ \leq ∥ y_{k_{j}} - T x_{k_{j}} ∥ + ∥ T x_{k_{j}} - y ∥ < 1 / (k_{j} + 1) + ∥ T x_{k_{j}} - y ∥$ , and both terms tend to $0$ , so $y_{k_{j}} \to y$ with $y \in C$ .

step 1.2step 2.2algebra

4.1

Thus every sequence in $C$ has a subsequence converging in $C$ , that is, $C$ is sequentially compact; by [A2] $C$ is compact, and then $T$ is compact by [A1].

step 3.2A1A2∎

Depends on

Used by

Dependency tree · two levels

95 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.2 p.183, Lemma 4.19 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §3.1 p.70, Theorem 3.2 (standard reference, not scraped)