OAI/Analysis/Pureness/Quasitrace/QuasitraceDistance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveQuasitrace.distance line 14
2. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_nonneg line 15
3. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_self line 16
4. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_comm line 17
5. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_star line 19
6. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_eq_zero_iff line 21
7. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_triangle line 26
8. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_add line 28
9. lemma OAI.CuntzPureness.PositiveQuasitrace.distance_mul line 31
10. def OAI.CuntzPureness.PositiveQuasitrace.pseudoMetricSpace line 40
11. def OAI.CuntzPureness.PositiveQuasitrace.faithfulMetricSpace line 46
12. def OAI.CuntzPureness.finiteSpectralQuasitracePseudoMetric line 56
13. def OAI.CuntzPureness.regularizedStateQuasitraceMetric line 60