OAI/Analysis/Commutator/DyadicDimension.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.DyadicPartition.lower line 25
2. def OAI.Kadison.PartialIsometryOrder.DyadicPartition.upper line 28
3. def OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension line 31
4. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.lower_nonneg line 33
5. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.lower_le_one line 36
6. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.lower_le_upper line 42
7. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.rank_succ_lower line 46
8. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.rank_succ_upper line 55
9. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.lower_monotone line 64
10. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.upper_antitone line 74
11. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.lower_le_dimension line 84
12. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_le_upper line 88
13. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_nonneg line 96
14. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_le_one line 99
15. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.upper_sub_lower line 104
16. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.lower_tendsto_dimension line 111
17. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_mono_subEquivalent line 116
18. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_congr_equivalent line 124
19. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_one line 131
20. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_zero line 136
21. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_pos line 142