OAI/CategoryTheory/Thomason/SquareClassification.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thomason.GrayTwo.eq_code_0 line 14
2. lemma OAI.Thomason.GrayTwo.eq_code_1 line 42
3. lemma OAI.Thomason.GrayTwo.eq_code_2 line 71
4. lemma OAI.Thomason.GrayTwo.eq_code_3 line 100
5. lemma OAI.Thomason.GrayTwo.eq_code_4 line 129
6. lemma OAI.Thomason.GrayTwo.eq_code_5 line 157
7. lemma OAI.Thomason.GrayTwo.eq_code_6 line 186
8. lemma OAI.Thomason.GrayTwo.eq_code_7 line 215
9. lemma OAI.Thomason.GrayTwo.eq_code_8 line 244
10. lemma OAI.Thomason.GrayTwo.eq_code_9 line 273
11. lemma OAI.Thomason.GrayTwo.eq_code_10 line 302
12. lemma OAI.Thomason.GrayTwo.eq_code_11 line 331
13. lemma OAI.Thomason.GrayTwo.eq_code_12 line 360
14. lemma OAI.Thomason.GrayTwo.eq_code_13 line 389
15. lemma OAI.Thomason.GrayTwo.eq_code_14 line 418
16. lemma OAI.Thomason.GrayTwo.eq_code_15 line 447
17. lemma OAI.Thomason.GrayTwo.eq_code_16 line 476
18. lemma OAI.Thomason.GrayTwo.eq_code_17 line 504
19. lemma OAI.Thomason.GrayTwo.eq_code_18 line 532
20. lemma OAI.Thomason.GrayTwo.eq_code_19 line 560
21. lemma OAI.Thomason.GrayTwo.eq_code_20 line 589
22. lemma OAI.Thomason.GrayTwo.eq_code_21 line 618
23. lemma OAI.Thomason.GrayTwo.eq_code_22 line 647
24. lemma OAI.Thomason.GrayTwo.impossible_10 line 675
25. lemma OAI.Thomason.GrayTwo.impossible_12 line 681
26. lemma OAI.Thomason.GrayTwo.impossible_20 line 687
27. lemma OAI.Thomason.GrayTwo.impossible_21 line 693
28. lemma OAI.Thomason.GrayTwo.impossible_30 line 699
29. lemma OAI.Thomason.GrayTwo.impossible_31 line 705
30. lemma OAI.Thomason.GrayTwo.impossible_32 line 711
31. lemma OAI.Thomason.GrayTwo.cases_01 line 717
32. lemma OAI.Thomason.GrayTwo.four_paths line 726
33. lemma OAI.Thomason.GrayTwo.cases_03 line 735
34. lemma OAI.Thomason.GrayTwo.cases_23 line 756
35. lemma OAI.Thomason.GrayTwo.has_vertex line 765
36. lemma OAI.Thomason.GrayTwo.is_code line 772