OAI/Analysis/Commutator/PartitionRankComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.piece_mul_part_of_mem line 26
2. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.piece_mul_part_of_not_mem line 33
3. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_injective line 36
4. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.card_le_of_part_subEquivalent line 52
5. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_subEquivalent_iff_card_le line 65
6. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_equivalent_iff_card_eq line 69