OAI/Analysis/KadisonKastler/ConjugateOutwardCuts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Two-vector projection cuts in the original algebra

  1. def OAI.KadisonKastler.finiteAlgebraOutwardProjection line 19
  2. theorem OAI.KadisonKastler.conjugationOperator_finiteOutward line 39
  3. theorem OAI.KadisonKastler.centralVectorDefect_projection line 48
  4. theorem OAI.KadisonKastler.exists_finite_two_vector_projection line 55