OAI/Analysis/KadisonKastler/ProjectionFamilySpaces.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Closed spaces attached to a family of projection cuts

The remaining left corner and the simultaneous commutation space are intersections of concrete operator kernels. Their projections therefore exist also for infinite families.

  1. def OAI.KadisonKastler.operatorKernelClosed line 22
  2. def OAI.KadisonKastler.projectionFamilyRemainderSpace line 24
  3. def OAI.KadisonKastler.projectionFamilyCommutationSpace line 27
  4. theorem OAI.KadisonKastler.mem_projectionFamilyRemainderSpace line 31
  5. theorem OAI.KadisonKastler.mem_projectionFamilyCommutationSpace line 36
  6. theorem OAI.KadisonKastler.projectionFamilyRemainderSpace_antitone line 44
  7. theorem OAI.KadisonKastler.projectionFamilyCommutationSpace_antitone line 50
  8. theorem OAI.KadisonKastler.projectionFamilyRemainderSpace_invariant line 56
  9. theorem OAI.KadisonKastler.projectionFamilyRemainderProjection_mem line 66
  10. def OAI.KadisonKastler.projectionFamilyRemainder line 76
  11. def OAI.KadisonKastler.projectionFamilyPinching line 82
  12. theorem OAI.KadisonKastler.projectionFamilyPinching_isProjection line 85