OAI/Analysis/Commutator/DyadicCuts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Kadison.PartialIsometryOrder.ProjectionIn line 20
2. def OAI.Kadison.PartialIsometryOrder.DyadicCuts.half line 30
3. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.half_square line 33
4. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.half_sum line 36
5. def OAI.Kadison.PartialIsometryOrder.DyadicCuts.next line 40
6. def OAI.Kadison.PartialIsometryOrder.DyadicCuts.cut line 45
7. def OAI.Kadison.PartialIsometryOrder.DyadicCuts.link line 49
8. def OAI.Kadison.PartialIsometryOrder.DyadicCuts.side line 51
9. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.cut_succ line 53
10. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.side_projection line 55
11. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.side_mem line 58
12. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.side_le line 61
13. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.cut_antitone line 64
14. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.cut_succ_add_side line 69
15. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.side_mul_cut_succ line 73
16. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.side_mul_side_of_lt line 81
17. lemma OAI.Kadison.PartialIsometryOrder.DyadicCuts.side_cross line 90
18. theorem OAI.Kadison.PartialIsometryOrder.DyadicCuts.exists_subEquivalent line 97