OAI/Analysis/KadisonKastler/ProjectionFamilyCut.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Adding a projection from the remaining corner

  1. theorem OAI.KadisonKastler.pairedProjectionCut_fixed_iff line 16
  2. theorem OAI.KadisonKastler.projectionFamily_conjugate_remainder_mul_pinching line 34
  3. theorem OAI.KadisonKastler.projectionFamily_subprojection_mul_pinching line 47