OAI/Analysis/Commutator/EqualProjectionPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Kadison.PartialIsometryOrder.EqualPartition line 22
2. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.triple line 41
3. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.final_projection line 44
4. lemma OAI.Kadison.PartialIsometryOrder.EqualPartition.final_cross line 48
5. def OAI.Kadison.PartialIsometryOrder.EqualPartition.matrixHom line 52
6. theorem OAI.Kadison.PartialIsometryOrder.EqualPartition.exists_double line 68
7. def OAI.Kadison.PartialIsometryOrder.EqualPartition.singleton line 134