OAI/Analysis/Pureness/Completion/CompletedTraceTracial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.completedDiagonalWeight_cut line 10
2. lemma OAI.CuntzPureness.completedDiagonalWeight_cut_le line 15
3. lemma OAI.CuntzPureness.completedProjection_conjugate_le line 20
4. lemma OAI.CuntzPureness.completedCornerCut_mono line 30
5. lemma OAI.CuntzPureness.completedCornerCut_mul_star_le line 35
6. lemma OAI.CuntzPureness.completedDiagonalWeight_finite_polar line 45
7. lemma OAI.CuntzPureness.completedDiagonalWeight_star_mul_le line 52
8. theorem OAI.CuntzPureness.completedDiagonalWeight_tracial line 61