OAI/Analysis/Pureness/Stabilization/MatrixRestriction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzTrace.matrixRestrict line 9
2. lemma OAI.CuntzTrace.matrixRestrict_self line 13
3. lemma OAI.CuntzTrace.matrixMask_eraseLast line 16
4. theorem OAI.CuntzTrace.matrixInclusion_restrict line 27
5. theorem OAI.CuntzTrace.matrixRestrict_norm_le line 38