OAI/Analysis/KadisonKastler/NormalPairAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A normal representation and the original algebra on their Hilbert sum

  1. def OAI.KadisonKastler.normalPairHom line 21
  2. theorem OAI.KadisonKastler.normalPairHom_injective line 24
  3. theorem OAI.KadisonKastler.normalPairHom_boundedWeakNormal line 32
  4. def OAI.KadisonKastler.normalPairAlgebra line 39
  5. def OAI.KadisonKastler.normalPairEquiv line 42
  6. theorem OAI.KadisonKastler.normalPairEquiv_coe line 47