OAI/Analysis/Commutator/EqualPartitionSums.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.EqualPartition.piece line 28
2. def OAI.Kadison.PartialIsometryOrder.EqualPartition.part line 30
3. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.piece_mem line 32
4. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.piece_projection line 34
5. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.piece_cross line 36
6. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_mem line 38
7. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_projection line 40
8. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_empty line 43
9. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_univ line 45
10. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_singleton line 47
11. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_insert line 49
12. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_mono line 52
13. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_le_one line 57
14. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_cross line 60
15. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.base_equiv_piece line 67
16. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.piece_equiv line 70
17. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_equiv_of_card_eq line 73
18. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_subEquivalent_of_card_le line 87
19. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.piece_ne_zero line 94
20. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_ne_zero_of_nonempty line 102