OAI/Analysis/KadisonKastler/CountableDiagonalAlgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The diagonal countable amplification as a represented von Neumann algebra

This preserves the ordinary near inclusion constant. Its faithful cyclic corner will put the first finite factor in standard position.

  1. def OAI.KadisonKastler.countableDiagonalAlgebra line 21
  2. theorem OAI.KadisonKastler.countableDiagonalHom_norm line 25
  3. theorem OAI.KadisonKastler.countableDiagonalHom_injective line 28
  4. theorem OAI.KadisonKastler.countableDiagonalHom_surjective_unitBall line 34
  5. theorem OAI.KadisonKastler.countableDiagonalHom_surjective line 67
  6. def OAI.KadisonKastler.countableDiagonalEquiv line 88
  7. theorem OAI.KadisonKastler.nearInclusion_countableDiagonal line 103