OAI/Analysis/Hyperinvariant/ProjectionBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Hyperinvariant.transitiveCommutant_of_invariantProjections line 11

   Source documentation

   Triviality of invariant projections in a von Neumann algebra implies hyperinvariant-subspace triviality in the entire bounded-operator algebra.

   theorem transitiveCommutant_of_invariantProjections
       (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) (hT : T ∈ M)
       (hproj : ∀ p ∈ M, IsStarProjection p → (1 - p) * T * p = 0 →
         p = 0 ∨ p = 1) : TransitiveCommutant T := by
   …

   Mentions: OAI.Hyperinvariant.TransitiveCommutant