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.
Kernel of identity minus compact is finite dimensional
Statement
Let be a normed space over or and let be a compact operator (Compact linear operator). Then the kernel
is a finite-dimensional subspace of : it admits an ordered basis of finite length (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).
Facts & Assumptions
is a bounded linear operator, and a bounded linear operator is continuous (A bounded linear operator between normed spaces, For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent); is compact, that is, is compact (Compact linear operator).
The normed space is a metric space with , convergence is metric convergence and limits of sequences are unique (Convergence of a sequence in a metric space: iff in , A sequence in a metric space has at most one limit, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, Complex norm and complex normed space, Realification preserves a complex norm and its metric); the closed unit ball is and is closed (Open ball, closed ball and sphere in a metric space, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).
If the closed unit ball of a normed space is compact, then that space admits an ordered basis of finite length (The closed unit ball is compact if and only if the normed space is finite-dimensional); a closed subset of a compact metric space is a compact metric subspace (A closed subset of a compact metric space is compact). Relative openness is the trace of ambient openness, and compactness is the compactness of the restricted metric (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).
Proof
Given: A normed space over or , a compact operator , and .
The set is a linear subspace of , since is linear. It is closed without using a sequential-closure criterion: take a bound for . If , put . For , the triangle inequality gives . Thus a ball around every lies outside , proving its complement open.
Every in the closed unit ball of satisfies and , hence ; therefore , and is a closed subset of by [step 1.1] and [A2].
The set is compact by [A1], so by [step 2.1] and [A3] the set is compact with its metric restricted from : it is relatively closed in the compact metric subspace . Restricting that same metric via gives exactly the same distance on , so it is also the compact closed unit ball of the normed space , so admits an ordered basis of finite length by [A3].
Hence is finite dimensional, as claimed.
Depends on
Compact linear operator
A bounded linear operator between normed spaces
For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent
The closed unit ball is compact if and only if the normed space is finite-dimensional
A closed subset of a compact metric space is compact
Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed
Convergence of a sequence in a metric space: iff in
A sequence in a metric space has at most one limit
Open ball, closed ball and sphere in a metric space
Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it
Complex norm and complex normed space
Realification preserves a complex norm and its metric