OAI/Analysis/KadisonKastler/FiniteOperatorAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finiteness of all operators forces finite Hilbert dimension

An infinite Hilbert basis admits a proper shift. The associated orthogonal sum is an isometry whose range misses one basis vector.

  1. theorem OAI.KadisonKastler.exists_injective_avoiding line 17
  2. theorem OAI.KadisonKastler.finiteDimensional_of_all_isometries_coisometric line 34