OAI/Analysis/Pureness/Cuntz/CuntzOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveCuntzClass.mk line 9
2. instance OAI.CuntzPureness.PositiveCuntzClass.(instance at line 11) line 11
3. theorem OAI.CuntzPureness.PositiveCuntzClass.mk_le_mk line 18
4. instance OAI.CuntzPureness.PositiveCuntzClass.partialOrder line 21
5. instance OAI.CuntzPureness.PositiveCuntzClass.(instance at line 38) line 38
6. instance OAI.CuntzPureness.PositiveCuntzClass.orderBot line 40
7. theorem OAI.CuntzPureness.PositiveCuntzClass.mk_eq_bot_iff line 45