OAI/Analysis/Pureness/Stabilization/Weights.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CuntzTrace.Positive line 10
  2. def OAI.CuntzTrace.Positive.zero line 13
  3. def OAI.CuntzTrace.Positive.add line 14
  4. def OAI.CuntzTrace.Positive.smul line 15
  5. def OAI.CuntzTrace.Positive.starMul line 17
  6. def OAI.CuntzTrace.Positive.mulStar line 18
  7. def OAI.CuntzTrace.Positive.sum line 19
  8. structure OAI.CuntzTrace.ExtendedTrace line 23
  9. instance OAI.CuntzTrace.ExtendedTrace.(instance at line 34) line 34
  10. theorem OAI.CuntzTrace.ExtendedTrace.ext line 36
  11. instance OAI.CuntzTrace.ExtendedTrace.(instance at line 42) line 42
  12. instance OAI.CuntzTrace.ExtendedTrace.(instance at line 50) line 50
  13. theorem OAI.CuntzTrace.ExtendedTrace.zero_apply line 65
  14. theorem OAI.CuntzTrace.ExtendedTrace.add_apply line 66
  15. instance OAI.CuntzTrace.ExtendedTrace.(instance at line 69) line 69
  16. theorem OAI.CuntzTrace.ExtendedTrace.monotone line 76
  17. theorem OAI.CuntzTrace.ExtendedTrace.zero_of_le line 86
  18. theorem OAI.CuntzTrace.ExtendedTrace.map_sum line 91
  19. theorem OAI.CuntzTrace.ExtendedTrace.finite_positive_partition line 102