OAI/Analysis/Commutator/DyadicPartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.EqualPartition.double line 27
2. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.double_base line 92
3. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.double_val line 95
4. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.base_ne_zero line 99
5. def OAI.Kadison.PartialIsometryOrder.DyadicPartition.Index line 116
6. instance OAI.Kadison.PartialIsometryOrder.DyadicPartition.indexFintype line 120
7. instance OAI.Kadison.PartialIsometryOrder.DyadicPartition.indexNonempty line 124
8. def OAI.Kadison.PartialIsometryOrder.DyadicPartition.partition line 128
9. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.cardinality line 136
10. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.base_eq_cut line 143
11. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.exists_base_subEquivalent line 157