OAI/Analysis/JiangSu/TraceCone/MatrixCorners.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TraceCone.MatrixCorners.matrixSuccessor_apply_castSucc line 15
2. lemma OAI.TraceCone.MatrixCorners.matrixSuccessor_injective line 22
3. lemma OAI.TraceCone.MatrixCorners.matrixSuccessor_isometry line 28
4. lemma OAI.TraceCone.MatrixCorners.matrixSuccessor_norm line 31
5. lemma OAI.TraceCone.MatrixCorners.matrixPad_self line 45
6. lemma OAI.TraceCone.MatrixCorners.matrixPad_trans line 49
7. lemma OAI.TraceCone.MatrixCorners.matrixInclusion_norm line 53
8. lemma OAI.TraceCone.MatrixCorners.matrixInclusion_isometry line 60
9. lemma OAI.TraceCone.MatrixCorners.matrixInclusion_trans line 64