OAI/Analysis/FreeWords/SupportProjections.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKSpectralSupport.rangeProjection line 19
  2. theorem OAI.KKSpectralSupport.rangeProjection_isProjection line 21
  3. theorem OAI.KKSpectralSupport.rangeProjection_mul line 24
  4. theorem OAI.KKSpectralSupport.mul_rangeProjection line 28
  5. theorem OAI.KKSpectralSupport.annihilate_rangeProjection line 32
  6. theorem OAI.KKSpectralSupport.rangeProjection_commute line 42
  7. theorem OAI.KKSpectralSupport.rangeProjection_mem line 47
  8. def OAI.KKSpectralSupport.supportProjection line 69
  9. theorem OAI.KKSpectralSupport.supportProjection_isProjection line 72
  10. theorem OAI.KKSpectralSupport.supportProjection_mul line 77
  11. theorem OAI.KKSpectralSupport.mul_supportProjection line 80
  12. theorem OAI.KKSpectralSupport.annihilate_supportProjection line 85
  13. theorem OAI.KKSpectralSupport.supportProjection_commute line 88
  14. theorem OAI.KKSpectralSupport.supportProjection_zero line 94
  15. theorem OAI.KKSpectralSupport.supportProjection_one line 98
  16. theorem OAI.KKSpectralSupport.supportProjection_le line 101