Aronszajn–Smith: compact operators have closed invariant subspaces

Theorem (von Neumann; Aronszajn–Smith 1954). Let $\mathbb{K}\in\{\mathbb{R},\mathbb{C}\}$, let $E$ be an infinite-dimensional Banach space over $\mathbb{K}$, and let $K\colon E\to E$ be a compact operator. Then $K$ has a non-trivial closed invariant subspace.

This was the first major positive result on the invariant subspace problem (von Neumann's unpublished Hilbert-space argument, published and extended to Banach spaces by Aronszajn and Smith).

Formalization Note The scalar field ranges over Mathlib's RCLike, covering both real and complex scalars; compactness is Mathlib's IsCompactOperator.