OAI/Analysis/Commutator/DyadicDimensionComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.PartialIsometryOrder.Link.equivalentSupports line 19
2. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_difference line 35
3. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_mono line 47
4. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_finset_sum line 52
5. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_base line 65
6. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.dimension_eq_zero_iff line 88
7. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.subEquivalent_of_dimension_le line 98
8. lemma OAI.Kadison.PartialIsometryOrder.DyadicPartition.equivalent_of_dimension_eq line 119