OAI/Analysis/Pureness/Comparison/TracialState.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CuntzComparison.TracialState line 11
  2. def OAI.CuntzComparison.TracialState.algebraicTrace line 19
  3. def OAI.CuntzComparison.TracialState.twoNorm line 23
  4. theorem OAI.CuntzComparison.TracialState.twoNorm_eq line 26
  5. theorem OAI.CuntzComparison.TracialState.twoNorm_nonneg line 30
  6. theorem OAI.CuntzComparison.TracialState.twoNorm_zero line 32
  7. theorem OAI.CuntzComparison.TracialState.twoNorm_one line 35
  8. theorem OAI.CuntzComparison.TracialState.twoNorm_add_le line 38
  9. theorem OAI.CuntzComparison.TracialState.twoNorm_smul line 43
  10. theorem OAI.CuntzComparison.TracialState.twoNorm_star line 47
  11. theorem OAI.CuntzComparison.TracialState.twoNorm_mul_left line 51
  12. theorem OAI.CuntzComparison.TracialState.twoNorm_mul_right line 63
  13. theorem OAI.CuntzComparison.TracialState.twoNorm_le_norm line 71
  14. def OAI.CuntzComparison.TracialState.toPreGNSContinuous line 74
  15. theorem OAI.CuntzComparison.TracialState.continuous_twoNorm line 79