OAI/Analysis/Pureness/Cuntz/FiniteCuntzStates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.sharedCuntz_isOrderedAddMonoid line 13
2. lemma OAI.CuntzPureness.sharedCuntz_zero_le line 16
3. instance OAI.CuntzPureness.finiteCuntz_isOrderedAddMonoid line 20
4. lemma OAI.CuntzPureness.finiteCuntz_zero_le line 23
5. def OAI.CuntzPureness.finitePositiveClass line 26
6. lemma OAI.CuntzPureness.finitePositiveClass_le_iff line 30
7. lemma OAI.CuntzPureness.finitePositiveClass_inclusion line 34
8. lemma OAI.CuntzPureness.finitePositiveClass_zero line 40
9. lemma OAI.CuntzPureness.finitePositiveClass_add line 46
10. theorem OAI.CuntzPureness.finiteCuntz_compare_of_buffer line 52
11. theorem OAI.CuntzPureness.finiteCuntz_state_gap_uniform line 63