OAI/Analysis/Commutator/PartitionRank.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.EqualPartition.rank line 27
2. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_le_card line 32
3. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.exists_rank line 36
4. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.card_le_rank_of_subEquivalent line 44
5. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_subEquivalent_of_card_le_rank line 49
6. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_subEquivalent_iff_card_le_rank line 55
7. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_mono_subEquivalent line 59
8. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_congr_equivalent line 65
9. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_mono line 70
10. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_part line 73
11. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_one line 81
12. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_zero line 87