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.
Compact linear operator
Definition
Let and be normed spaces over the same scalar field , read in the real case from A norm on a real vector space, the induced metric, and the dictionary with the metric axioms and in the complex case from Complex norm and complex normed space. A linear map (Linear map between vector spaces over the same field) is a compact operator when the image of every bounded subset of (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space) has compact closure in (Open cover, subcover, compact metric space, and compact subset of a metric space); explicitly, for every bounded the closure in is a compact subset of . The set of compact operators is written . The metric used here is , supplied over by A norm on a real vector space, the induced metric, and the dictionary with the metric axioms and over by Realification preserves a complex norm and its metric.
The closed unit ball suffices. Put (Open ball, closed ball and sphere in a metric space). Then is compact if and only if is a compact subset of .
Indeed, if is compact then is bounded, because while is bounded and a subset of a bounded set is bounded, so has compact closure. Conversely assume compact and let be bounded. If then , whose closure is empty and hence compact. Otherwise for some and real , so every satisfies ; if then and if then , so in either case . Scalar multiplication by is continuous (Vector addition and scalar multiplication are continuous in a normed space), so is a compact subset of (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), hence closed (A compact subset of a metric space is closed and bounded); therefore is a closed subset of a compact set, hence compact, and is compact.
A compact operator is bounded. If is compact then the compact set is bounded (A compact subset of a metric space is closed and bounded), so there is a real with for every and hence for every ; thus is a bounded linear operator (A bounded linear operator between normed spaces). This is a consequence of compactness, not a hypothesis of the definition.
Depends on
A bounded linear operator between normed spaces
Open cover, subcover, compact metric space, and compact subset of a metric space
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
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
Complex norm and complex normed space
Linear map between vector spaces over the same field
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
A compact subset of a metric space is closed and bounded
Vector addition and scalar multiplication are continuous in a normed space
Realification preserves a complex norm and its metric