OAI/Analysis/Commutator/TracialSequence.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.TracialSequence.vectorCLM line 26
  2. lemma OAI.Kadison.TracialSequence.vectorCLM_apply line 34
  3. def OAI.Kadison.TracialSequence.vectorPre line 36
  4. lemma OAI.Kadison.TracialSequence.vectorPre_seq line 39
  5. def OAI.Kadison.TracialSequence.vector line 42
  6. lemma OAI.Kadison.TracialSequence.vector_eq_zero_iff line 59
  7. def OAI.Kadison.TracialSequence.boundedSubspace line 63
  8. instance OAI.Kadison.TracialSequence.(instance at line 65) line 65
  9. lemma OAI.Kadison.TracialSequence.vector_mem line 68
  10. def OAI.Kadison.TracialSequence.leftFamily line 71
  11. lemma OAI.Kadison.TracialSequence.leftFamily_apply line 78
  12. lemma OAI.Kadison.TracialSequence.norm_leftFamily_le line 80
  13. def OAI.Kadison.TracialSequence.leftHom line 85
  14. lemma OAI.Kadison.TracialSequence.leftHom_vector line 95
  15. lemma OAI.Kadison.TracialSequence.leftHom_preserves line 107
  16. def OAI.Kadison.TracialSequence.leftRestricted line 117
  17. lemma OAI.Kadison.TracialSequence.leftRestricted_apply line 120
  18. lemma OAI.Kadison.TracialSequence.vector_mul_norm line 126
  19. lemma OAI.Kadison.TracialSequence.vector_mul_zero line 133
  20. lemma OAI.Kadison.TracialSequence.left_null line 143