OAI/Analysis/Commutator/OrthogonalRank.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_union line 29
2. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.part_compl line 32
3. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.rank_add_le_card line 41
4. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.orthogonal_rank_lower line 59
5. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.subEquivalent_part_of_rank_lt line 79
6. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.orthogonal_rank_upper line 86