Invariant Subspace Problem

Exact retained declaration excerpt — not the whole file.

/--
Show that every bounded linear operator `T : H → H` on a separable Hilbert space `H` of dimension
at least 2 has a non-trivial closed `T`-invariant subspace: a closed linear subspace `W` of `H`,
which is different from `H` and from `{0}`, such that `T ( W ) ⊂ W`. One needs the assumption that
the dimension of `H` is at least 2 because otherwise any subspace would be either `H` or `{0}`. -/
@[category research open, AMS 47]
theorem Invariant_subspace_problem [InnerProductSpace ℂ H] [TopologicalSpace.SeparableSpace H]
    [CompleteSpace H] (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) :
    Nonempty (ClosedInvariantSubspace T) := by
  sorry