OAI/Analysis/Commutator/ProjectionJoin.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.ProjectionJoin.remainder line 21
2. def OAI.Kadison.ProjectionJoin.join line 23
3. lemma OAI.Kadison.ProjectionJoin.remainder_projection line 25
4. lemma OAI.Kadison.ProjectionJoin.remainder_le line 28
5. lemma OAI.Kadison.ProjectionJoin.remainder_mul line 33
6. lemma OAI.Kadison.ProjectionJoin.mul_remainder line 39
7. lemma OAI.Kadison.ProjectionJoin.join_projection line 44
8. lemma OAI.Kadison.ProjectionJoin.left_le line 51
9. lemma OAI.Kadison.ProjectionJoin.right_le line 56
10. lemma OAI.Kadison.ProjectionJoin.join_le line 66
11. lemma OAI.Kadison.ProjectionJoin.remainder_mem line 77
12. lemma OAI.Kadison.ProjectionJoin.join_mem line 80
13. theorem OAI.Kadison.ProjectionJoin.dimension_join_le line 89