OAI/Analysis/KadisonKastler/PartialSupportSpan.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The projection onto the closed span of the initial spaces of a family of partial isometries. All constructions remain in the original algebra.

  1. def OAI.KadisonKastler.partialSupportVectors line 18
  2. def OAI.KadisonKastler.partialSupportSpace line 21
  3. instance OAI.KadisonKastler.partialSupportSpace_complete line 24
  4. theorem OAI.KadisonKastler.partialSupportSpace_le_ker line 28
  5. theorem OAI.KadisonKastler.partialSupportProjection_mem line 37
  6. def OAI.KadisonKastler.partialSupportProjection line 55
  7. theorem OAI.KadisonKastler.support_le_partialSupportProjection line 63
  8. theorem OAI.KadisonKastler.partialSupportProjection_le line 70
  9. theorem OAI.KadisonKastler.support_le_centralSupport_of_target_le line 83