OAI/Analysis/JiangSu/CuntzSemigroup/FiniteCuntzStates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Pureness.sharedCuntz_isOrderedAddMonoid line 19
  2. lemma OAI.Pureness.sharedCuntz_zero_le line 22
  3. instance OAI.Pureness.finiteCuntz_isOrderedAddMonoid line 26
  4. lemma OAI.Pureness.finiteCuntz_zero_le line 29
  5. def OAI.Pureness.finitePositiveClass line 32
  6. lemma OAI.Pureness.finitePositiveClass_le_iff line 36
  7. lemma OAI.Pureness.finitePositiveClass_inclusion line 40
  8. lemma OAI.Pureness.finitePositiveClass_zero line 46
  9. lemma OAI.Pureness.finitePositiveClass_add line 55
  10. theorem OAI.Pureness.finiteCuntz_compare_of_buffer line 61
  11. theorem OAI.Pureness.finiteCuntz_state_gap_uniform line 72