OAI/Analysis/JiangSu/Traceless/TracelessStabilizedPure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentMain.Traceless.compress_norm_le line 18
2. theorem OAI.CurrentMain.Traceless.cuntz_reflect_corner line 27
3. theorem OAI.CurrentMain.Traceless.cuntz_reflect_spatial line 63
4. instance OAI.CurrentMain.Traceless.spatialStabilizationOrder line 69
5. instance OAI.CurrentMain.Traceless.spatialStabilizationStarOrdered line 72
6. theorem OAI.CurrentMain.Traceless.infinite_projection_of_stabilized_comparison line 75
7. def OAI.CurrentMain.Traceless.IsHereditary line 103
8. lemma OAI.CurrentMain.Traceless.IsHereditary.sandwich line 106
9. lemma OAI.CurrentMain.Traceless.IsHereditary.principal_le line 124
10. def OAI.CurrentMain.Traceless.IsInfiniteProjectionIn line 132
11. lemma OAI.CurrentMain.Traceless.IsHereditary.infiniteProjectionIn line 136
12. theorem OAI.CurrentMain.Traceless.infinite_projection_in_nonzero_hereditary line 143