OAI/Analysis/Commutator/ProjectionShift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.ProjectionShift.partialSum line 22
2. lemma OAI.Kadison.ProjectionShift.conjugate_projection line 28
3. lemma OAI.Kadison.ProjectionShift.partial_projection_le line 38
4. lemma OAI.Kadison.ProjectionShift.partial_mono line 50
5. lemma OAI.Kadison.ProjectionShift.partial_mem line 57
6. theorem OAI.Kadison.ProjectionShift.exists_fixed_projection line 63