OAI/Analysis/Commutator/ProjectionAddition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.Link.orthogonalSum line 22
2. lemma OAI.Kadison.PartialIsometryOrder.Link.orthogonalSum_initial line 41
3. lemma OAI.Kadison.PartialIsometryOrder.Link.orthogonalSum_final line 50
4. lemma OAI.Kadison.PartialIsometryOrder.SubEquivalent.orthogonal_add line 61
5. lemma OAI.Kadison.PartialIsometryOrder.Equivalent.orthogonal_add line 72
6. theorem OAI.Kadison.PartialIsometryOrder.subEquivalent_unitary line 84