OAI/Analysis/BoundedHochschild/CountableMatrixSubalgebra.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The von Neumann algebra generated by a countable matrix system contains all finite unital isometry columns. The ambient countable columns themselves need not belong to this generated algebra.

  1. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixAlgebra line 20
  2. def OAI.BoundedHochschild.KadisonRingrose.matrixClosureStarPreadjoint line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.matrixClosureStarPreadjoint_spec line 27
  4. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure line 31
  5. instance OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_closed line 38
  6. instance OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_wstar line 43
  7. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_transition line 49
  8. theorem OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_columns line 55