OAI/Analysis/JiangSu/Comparison/Corner.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectComparison.cornerProjection_mul_corner line 21
2. lemma OAI.DirectComparison.corner_mul_cornerProjection line 28
3. lemma OAI.DirectComparison.corner_compressed_sandwich line 35
4. lemma OAI.DirectComparison.compress_corner_sandwich line 48
5. theorem OAI.DirectComparison.hereditary_corner_reflect line 53
6. lemma OAI.DirectComparison.map_mem_hereditary line 73
7. def OAI.DirectComparison.scalarCorner line 84
8. lemma OAI.DirectComparison.scalarCorner_apply line 87
9. lemma OAI.DirectComparison.scalarCorner_injective line 90
10. lemma OAI.DirectComparison.scalarCorner_isometry line 93
11. lemma OAI.DirectComparison.scalarCorner_nonneg line 96
12. lemma OAI.DirectComparison.scalarCorner_norm line 99
13. lemma OAI.DirectComparison.matrixTrace_scalarCorner line 102
14. lemma OAI.DirectComparison.scalarCorner_trace line 108
15. lemma OAI.DirectComparison.scalarCorner_trace_scale line 116
16. lemma OAI.DirectComparison.matrixRank_scalarCorner line 122
17. theorem OAI.DirectComparison.hereditary_scalarCorner_reflect line 134
18. lemma OAI.DirectComparison.trace_lt_rank_of_norm_lt_one line 162
19. lemma OAI.DirectComparison.matrix_approximant_cuntzBelow line 177
20. theorem OAI.DirectComparison.almost_projection line 196