OAI/Analysis/Pureness/Completion/CompletedCornerRange.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.completedCornerCut_finite_range line 9
  2. theorem OAI.CuntzPureness.completedCornerCut_mem_range line 19
  3. def OAI.CuntzPureness.completedCompress line 30
  4. lemma OAI.CuntzPureness.include_completedCompress line 33
  5. lemma OAI.CuntzPureness.completedCompress_continuous line 37
  6. lemma OAI.CuntzPureness.completedCompress_norm_le line 41
  7. lemma OAI.CuntzPureness.completedCompress_include line 46
  8. lemma OAI.CuntzPureness.completedProjection_mul_include line 51
  9. lemma OAI.CuntzPureness.include_mul_completedProjection line 56
  10. lemma OAI.CuntzPureness.completedCornerCut_sandwich line 61
  11. lemma OAI.CuntzPureness.completedCompress_sandwich line 68
  12. theorem OAI.CuntzPureness.cuntzSubequiv_completedMatrixInclude_iff line 75