OAI/Analysis/Pureness/Stabilization/CuntzClass.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzTrace.cuntzSetoid line 9
2. def OAI.CuntzTrace.CuntzClass line 14
3. def OAI.CuntzTrace.CuntzClass.mk line 18
4. instance OAI.CuntzTrace.CuntzClass.(instance at line 20) line 20
5. theorem OAI.CuntzTrace.CuntzClass.mk_le_mk line 25
6. instance OAI.CuntzTrace.CuntzClass.(instance at line 27) line 27
7. theorem OAI.CuntzTrace.CuntzClass.mk_eq_mk_iff line 33
8. def OAI.CuntzTrace.ExtendedTrace.cuntzRank line 40
9. theorem OAI.CuntzTrace.ExtendedTrace.cuntzRank_mk line 46