OAI/Analysis/KadisonKastler/CompleteLinearOperations.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Elementary operations on complete bounds

  1. theorem OAI.KadisonKastler.matrix_map_add line 16
  2. theorem OAI.KadisonKastler.matrix_map_zero line 23
  3. theorem OAI.KadisonKastler.CompletelyBoundedBy.mono line 28
  4. theorem OAI.KadisonKastler.CompletelyBoundedBy.add line 33
  5. theorem OAI.KadisonKastler.CompletelyBoundedBy.sub line 40
  6. theorem OAI.KadisonKastler.completelyBoundedBy_id line 47
  7. theorem OAI.KadisonKastler.CompletelyBoundedBy.comp line 51
  8. theorem OAI.KadisonKastler.CompletelyBoundedBy.opNorm_le line 58