OAI/Analysis/Commutator/ProjectionLifts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.ProjectionLifts.halfCut line 25
2. lemma OAI.Kadison.ProjectionLifts.isProjection_halfCut line 27
3. lemma OAI.Kadison.ProjectionLifts.rounding line 34
4. def OAI.Kadison.ProjectionLifts.roundedSequence line 40
5. lemma OAI.Kadison.ProjectionLifts.roundedSequence_apply line 44
6. lemma OAI.Kadison.ProjectionLifts.roundedSequence_projection line 47
7. theorem OAI.Kadison.ProjectionLifts.projection_lift line 58