OAI/Analysis/Pureness/Quasitrace/QuasitraceBoundedCompletion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CuntzPureness.PositiveQuasitrace.MetricPoint line 12
  2. instance OAI.CuntzPureness.PositiveQuasitrace.metricPointPseudoMetric line 16
  3. def OAI.CuntzPureness.PositiveQuasitrace.BoundedPoint line 22
  4. instance OAI.CuntzPureness.PositiveQuasitrace.boundedPointPseudoMetric line 23
  5. abbrev OAI.CuntzPureness.PositiveQuasitrace.BoundedCompletion line 26
  6. def OAI.CuntzPureness.PositiveQuasitrace.boundedStar line 28
  7. def OAI.CuntzPureness.PositiveQuasitrace.boundedAdd line 30
  8. def OAI.CuntzPureness.PositiveQuasitrace.boundedMul line 32
  9. lemma OAI.CuntzPureness.PositiveQuasitrace.boundedStar_isometry line 36
  10. lemma OAI.CuntzPureness.PositiveQuasitrace.boundedAdd_lipschitz line 40
  11. lemma OAI.CuntzPureness.PositiveQuasitrace.boundedMul_lipschitz line 50
  12. def OAI.CuntzPureness.PositiveQuasitrace.completedBoundedStar line 69
  13. def OAI.CuntzPureness.PositiveQuasitrace.completedBoundedAdd line 71
  14. def OAI.CuntzPureness.PositiveQuasitrace.completedBoundedMul line 74
  15. lemma OAI.CuntzPureness.PositiveQuasitrace.completedBoundedStar_coe line 78
  16. lemma OAI.CuntzPureness.PositiveQuasitrace.completedBoundedAdd_coe line 81
  17. lemma OAI.CuntzPureness.PositiveQuasitrace.completedBoundedMul_coe line 85