OAI/Analysis/Pureness/Comparison/MatrixCornerFunctionals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzComparison.matrixCornerExtract_continuous line 13
2. lemma OAI.CuntzComparison.matrixCornerExtract_nonneg line 18
3. lemma OAI.CuntzComparison.matrixCornerProjection_mul line 26
4. lemma OAI.CuntzComparison.matrixCornerProjection_mul_rev line 31
5. lemma OAI.CuntzComparison.matrixCompression_nested line 36
6. lemma OAI.CuntzComparison.matrixCornerExtract_stage_large line 43
7. lemma OAI.CuntzComparison.matrixCornerExtract_stage_small line 49
8. lemma OAI.CuntzComparison.matrixCornerExtract_coherent line 55
9. def OAI.CuntzComparison.TracialState.matrixCornerFunctional line 61
10. lemma OAI.CuntzComparison.TracialState.matrixCornerFunctional_apply line 71
11. theorem OAI.CuntzComparison.TracialState.matrixCornerFunctional_monotone line 74