OAI/Combinatorics/Ramsey/CycleClique/Construction/CoverageK8.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover5 line 8
  2. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover4 line 12
  3. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover6 line 18
  4. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover7 line 22
  5. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover8 line 26
  6. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover9 line 30
  7. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover3 line 34
  8. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover10 line 56
  9. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover11 line 62
  10. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover12 line 66
  11. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover13 line 70
  12. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover14 line 74
  13. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover15 line 80
  14. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover16 line 84
  15. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover17 line 90
  16. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover2 line 96
  17. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover19 line 152
  18. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover20 line 156
  19. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover21 line 160
  20. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover18 line 164
  21. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover22 line 183
  22. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover23 line 189
  23. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover24 line 193
  24. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover25 line 197
  25. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover26 line 203
  26. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover27 line 207
  27. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover29 line 213
  28. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover28 line 217
  29. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover30 line 233
  30. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover31 line 239
  31. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover32 line 252
  32. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t4_cover1 line 262
  33. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k8_t4 line 354
  34. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover6 line 358
  35. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover5 line 362
  36. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover7 line 368
  37. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover8 line 372
  38. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover9 line 376
  39. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover4 line 380
  40. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover10 line 399
  41. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover11 line 405
  42. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover12 line 409
  43. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover13 line 413
  44. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover14 line 419
  45. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover3 line 425
  46. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover16 line 465
  47. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover17 line 469
  48. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover15 line 473
  49. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover18 line 489
  50. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover19 line 495
  51. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover20 line 499
  52. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover21 line 505
  53. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover22 line 518
  54. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover2 line 528
  55. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover24 line 583
  56. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover25 line 589
  57. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover26 line 593
  58. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover23 line 599
  59. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover27 line 626
  60. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover28 line 639
  61. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover29 line 645
  62. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover30 line 655
  63. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover31 line 672
  64. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t5_cover1 line 682
  65. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k8_t5 line 741
  66. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover7 line 745
  67. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover6 line 749
  68. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover8 line 755
  69. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover9 line 759
  70. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover5 line 763
  71. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover10 line 779
  72. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover11 line 785
  73. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover12 line 789
  74. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover4 line 795
  75. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover14 line 822
  76. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover13 line 826
  77. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover15 line 839
  78. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover16 line 845
  79. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover3 line 855
  80. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover18 line 886
  81. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover17 line 892
  82. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover19 line 909
  83. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover20 line 919
  84. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover2 line 929
  85. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover22 line 960
  86. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover21 line 970
  87. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover23 line 987
  88. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover24 line 997
  89. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t6_cover1 line 1007
  90. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k8_t6 line 1038
  91. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover8 line 1042
  92. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover7 line 1046
  93. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover9 line 1052
  94. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover6 line 1056
  95. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover10 line 1069
  96. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover5 line 1075
  97. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover11 line 1092
  98. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover4 line 1102
  99. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover12 line 1119
  100. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover3 line 1129
  101. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover13 line 1146
  102. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover2 line 1156
  103. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover14 line 1173
  104. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t7_cover1 line 1183
  105. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k8_t7 line 1200
  106. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover9 line 1204
  107. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover8 line 1208
  108. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover7 line 1214
  109. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover6 line 1224
  110. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover5 line 1234
  111. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover4 line 1244
  112. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover3 line 1254
  113. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover2 line 1264
  114. theorem OAI.CycleClique.Construction.CertifiedCoverage.k8t8_cover1 line 1274
  115. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k8_t8 line 1284