OAI/Analysis/JiangSu/MatrixAlgebras/MatrixUnitCorners.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UnitalTomsWinter.matrixCornerProjection line 18
2. lemma OAI.UnitalTomsWinter.matrixCornerProjection_isStarProjection line 20
3. lemma OAI.UnitalTomsWinter.matrixInclusion_one_mul line 28
4. theorem OAI.UnitalTomsWinter.matrixCompression_eq_corner line 45
5. theorem OAI.UnitalTomsWinter.matrixLimitStage_full_corner line 71
6. theorem OAI.UnitalTomsWinter.cuntzSubequiv_reflect_matrixLimit line 77