OAI/Analysis/Pureness/Quasitrace/QuasitraceCauchy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.PositiveQuasitrace.IsMetricCauchy line 12
  2. def OAI.CuntzPureness.PositiveQuasitrace.IsMetricNull line 14
  3. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricCauchy_const line 16
  4. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricCauchy_star line 18
  5. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricCauchy_neg line 21
  6. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricCauchy_smul line 27
  7. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricNull_zero line 31
  8. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricNull_star line 33
  9. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricNull_neg line 35
  10. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricNull_smul line 37
  11. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricNull_mul_left line 41
  12. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricNull_mul_right line 50
  13. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricCauchy_add line 59
  14. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricNull_add line 63
  15. lemma OAI.CuntzPureness.PositiveQuasitrace.isMetricCauchy_mul line 67