OAI/Analysis/KadisonKastler/RelativeMatrixExtension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Extending a finite matrix stage inside its relative commutant

  1. theorem OAI.KadisonKastler.matrix_concrete_mono line 16
  2. theorem OAI.KadisonKastler.matrix_relative_commutes line 24
  3. def OAI.KadisonKastler.relativeMatrixExtension line 32
  4. theorem OAI.KadisonKastler.relativeMatrixExtension_algebra line 41
  5. theorem OAI.KadisonKastler.relativeMatrixExtension_contains_left line 51
  6. theorem OAI.KadisonKastler.relativeMatrixExtension_contains_right line 58
  7. theorem OAI.KadisonKastler.TypeIIIFactor.exists_matrixStage_extension_containing_projection line 77