OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientValue.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveQuasitrace.cauchyValue line 14
2. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyValue_tendsto line 17
3. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyValue_congr line 22
4. def OAI.CuntzPureness.PositiveQuasitrace.quotientValue line 31
5. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_map line 34
6. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_embedding line 36
7. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyValue_polar line 41
8. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_polar line 52
9. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientValue_square_nonneg line 58