Back to Problems

Invariant_subspace_problem_non_separable

Specification

Every bounded linear operator `T : H → H` on a non-separable Hilbert space `H` has a non-trivial closed `T`-invariant subspace. Such an invariant space is given by considering the closure of the linear span of the orbit of any single non-zero vector.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem Invariant_subspace_problem_non_separable [InnerProductSpace ℂ H] [CompleteSpace H]
    (h : ¬TopologicalSpace.SeparableSpace H) (T : H →L[ℂ] H) :
    Nonempty (ClosedInvariantSubspace T)
ID: Wikipedia__InvariantSubspaceProblem__Invariant_subspace_problem_non_separable
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.