OAI/Analysis/JiangSu/Comparison/CuntzBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UnitalTomsWinter.CuntzSubequiv line 14
  2. theorem OAI.UnitalTomsWinter.cuntzSubequiv_iff_sequence line 17
  3. theorem OAI.UnitalTomsWinter.cuntzSubequiv_iff_norm line 28
  4. theorem OAI.UnitalTomsWinter.cuntzSubequiv_of_exact line 34
  5. theorem OAI.UnitalTomsWinter.zero_cuntzSubequiv line 38
  6. theorem OAI.UnitalTomsWinter.cuntzSubequiv_zero_iff line 41
  7. theorem OAI.UnitalTomsWinter.CuntzSubequiv.of_tendsto line 44
  8. theorem OAI.UnitalTomsWinter.CuntzSubequiv.compress line 49
  9. theorem OAI.UnitalTomsWinter.CuntzSubequiv.trans line 57
  10. lemma OAI.UnitalTomsWinter.projection_norm_le_one line 72
  11. lemma OAI.UnitalTomsWinter.projection_compression_norm_le line 75
  12. theorem OAI.UnitalTomsWinter.CuntzSubequiv.exists_corner_witness line 83