OAI/Analysis/Pureness/Cuntz/CuntzSubequivalence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.CuntzSubequiv line 12
  2. theorem OAI.CuntzPureness.cuntzSubequiv_iff_sequence line 15
  3. theorem OAI.CuntzPureness.cuntzSubequiv_iff_norm line 26
  4. theorem OAI.CuntzPureness.cuntzSubequiv_conjugate line 38
  5. theorem OAI.CuntzPureness.zero_cuntzSubequiv line 41
  6. theorem OAI.CuntzPureness.cuntzSubequiv_of_tendsto line 44
  7. theorem OAI.CuntzPureness.CuntzSubequiv.conjugate_left line 49
  8. theorem OAI.CuntzPureness.CuntzSubequiv.trans line 59
  9. theorem OAI.CuntzPureness.cuntzSubequiv_zero_iff line 64
  10. theorem OAI.CuntzPureness.cuntzSubequiv_refl line 69
  11. def OAI.CuntzPureness.cuntzSetoid line 72