OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientMetric.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize line 13
  2. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_nonneg line 16
  3. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_cube line 19
  4. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_zero line 23
  5. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_eq_zero_iff line 27
  6. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_neg line 39
  7. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_star line 43
  8. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_map_tendsto line 47
  9. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_add line 60
  10. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSize_embedding line 70
  11. def OAI.CuntzPureness.PositiveQuasitrace.quotientDistance line 74
  12. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientDistance_nonneg line 75
  13. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientDistance_self line 77
  14. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientDistance_comm line 79
  15. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientDistance_triangle line 82
  16. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientDistance_eq_zero_iff line 85
  17. def OAI.CuntzPureness.PositiveQuasitrace.quotientMetricSpace line 90
  18. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientDistance_embedding line 97
  19. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientDistance_map_tendsto line 101