OAI/Combinatorics/Ramsey/CycleClique/Certificates010.lean

GitHub source file

219 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_288_q line 20
  2. def OAI.CycleClique.certificate_288_edges line 21
  3. def OAI.CycleClique.certificate_288_part_0 line 23
  4. def OAI.CycleClique.certificate_288_part_1 line 25
  5. def OAI.CycleClique.certificate_288 line 27
  6. theorem OAI.CycleClique.certificate_288_checked line 29
  7. theorem OAI.CycleClique.certificate_288_valid line 30
  8. def OAI.CycleClique.certificate_289_q line 32
  9. def OAI.CycleClique.certificate_289_edges line 33
  10. def OAI.CycleClique.certificate_289_part_0 line 35
  11. def OAI.CycleClique.certificate_289_part_1 line 37
  12. def OAI.CycleClique.certificate_289 line 39
  13. theorem OAI.CycleClique.certificate_289_checked line 41
  14. theorem OAI.CycleClique.certificate_289_valid line 42
  15. def OAI.CycleClique.certificate_290_q line 44
  16. def OAI.CycleClique.certificate_290_edges line 45
  17. def OAI.CycleClique.certificate_290_part_0 line 47
  18. def OAI.CycleClique.certificate_290_part_1 line 49
  19. def OAI.CycleClique.certificate_290 line 51
  20. theorem OAI.CycleClique.certificate_290_checked line 53
  21. theorem OAI.CycleClique.certificate_290_valid line 54
  22. def OAI.CycleClique.certificate_291_q line 56
  23. def OAI.CycleClique.certificate_291_edges line 57
  24. def OAI.CycleClique.certificate_291_part_0 line 59
  25. def OAI.CycleClique.certificate_291 line 61
  26. theorem OAI.CycleClique.certificate_291_checked line 63
  27. theorem OAI.CycleClique.certificate_291_valid line 64
  28. def OAI.CycleClique.certificate_292_q line 66
  29. def OAI.CycleClique.certificate_292_edges line 67
  30. def OAI.CycleClique.certificate_292_part_0 line 69
  31. def OAI.CycleClique.certificate_292 line 71
  32. theorem OAI.CycleClique.certificate_292_checked line 73
  33. theorem OAI.CycleClique.certificate_292_valid line 74
  34. def OAI.CycleClique.certificate_293_q line 76
  35. def OAI.CycleClique.certificate_293_edges line 77
  36. def OAI.CycleClique.certificate_293_part_0 line 79
  37. def OAI.CycleClique.certificate_293_part_1 line 81
  38. def OAI.CycleClique.certificate_293 line 83
  39. theorem OAI.CycleClique.certificate_293_checked line 85
  40. theorem OAI.CycleClique.certificate_293_valid line 86
  41. def OAI.CycleClique.certificate_294_q line 88
  42. def OAI.CycleClique.certificate_294_edges line 89
  43. def OAI.CycleClique.certificate_294_part_0 line 91
  44. def OAI.CycleClique.certificate_294_part_1 line 93
  45. def OAI.CycleClique.certificate_294 line 95
  46. theorem OAI.CycleClique.certificate_294_checked line 97
  47. theorem OAI.CycleClique.certificate_294_valid line 98
  48. def OAI.CycleClique.certificate_295_q line 100
  49. def OAI.CycleClique.certificate_295_edges line 101
  50. def OAI.CycleClique.certificate_295_part_0 line 103
  51. def OAI.CycleClique.certificate_295 line 105
  52. theorem OAI.CycleClique.certificate_295_checked line 107
  53. theorem OAI.CycleClique.certificate_295_valid line 108
  54. def OAI.CycleClique.certificate_296_q line 110
  55. def OAI.CycleClique.certificate_296_edges line 111
  56. def OAI.CycleClique.certificate_296_part_0 line 113
  57. def OAI.CycleClique.certificate_296_part_1 line 115
  58. def OAI.CycleClique.certificate_296 line 117
  59. theorem OAI.CycleClique.certificate_296_checked line 119
  60. theorem OAI.CycleClique.certificate_296_valid line 120
  61. def OAI.CycleClique.certificate_297_q line 122
  62. def OAI.CycleClique.certificate_297_edges line 123
  63. def OAI.CycleClique.certificate_297_part_0 line 125
  64. def OAI.CycleClique.certificate_297_part_1 line 127
  65. def OAI.CycleClique.certificate_297 line 129
  66. theorem OAI.CycleClique.certificate_297_checked line 131
  67. theorem OAI.CycleClique.certificate_297_valid line 132
  68. def OAI.CycleClique.certificate_298_q line 134
  69. def OAI.CycleClique.certificate_298_edges line 135
  70. def OAI.CycleClique.certificate_298_part_0 line 137
  71. def OAI.CycleClique.certificate_298_part_1 line 139
  72. def OAI.CycleClique.certificate_298 line 141
  73. theorem OAI.CycleClique.certificate_298_checked line 143
  74. theorem OAI.CycleClique.certificate_298_valid line 144
  75. def OAI.CycleClique.certificate_299_q line 146
  76. def OAI.CycleClique.certificate_299_edges line 147
  77. def OAI.CycleClique.certificate_299_part_0 line 149
  78. def OAI.CycleClique.certificate_299_part_1 line 151
  79. def OAI.CycleClique.certificate_299 line 153
  80. theorem OAI.CycleClique.certificate_299_checked line 155
  81. theorem OAI.CycleClique.certificate_299_valid line 156
  82. def OAI.CycleClique.certificate_300_q line 158
  83. def OAI.CycleClique.certificate_300_edges line 159
  84. def OAI.CycleClique.certificate_300_part_0 line 161
  85. def OAI.CycleClique.certificate_300_part_1 line 163
  86. def OAI.CycleClique.certificate_300 line 165
  87. theorem OAI.CycleClique.certificate_300_checked line 167
  88. theorem OAI.CycleClique.certificate_300_valid line 168
  89. def OAI.CycleClique.certificate_301_q line 170
  90. def OAI.CycleClique.certificate_301_edges line 171
  91. def OAI.CycleClique.certificate_301_part_0 line 173
  92. def OAI.CycleClique.certificate_301_part_1 line 175
  93. def OAI.CycleClique.certificate_301 line 177
  94. theorem OAI.CycleClique.certificate_301_checked line 179
  95. theorem OAI.CycleClique.certificate_301_valid line 180
  96. def OAI.CycleClique.certificate_302_q line 182
  97. def OAI.CycleClique.certificate_302_edges line 183
  98. def OAI.CycleClique.certificate_302_part_0 line 185
  99. def OAI.CycleClique.certificate_302_part_1 line 187
  100. def OAI.CycleClique.certificate_302 line 189
  101. theorem OAI.CycleClique.certificate_302_checked line 191
  102. theorem OAI.CycleClique.certificate_302_valid line 192
  103. def OAI.CycleClique.certificate_303_q line 194
  104. def OAI.CycleClique.certificate_303_edges line 195
  105. def OAI.CycleClique.certificate_303_part_0 line 197
  106. def OAI.CycleClique.certificate_303_part_1 line 199
  107. def OAI.CycleClique.certificate_303 line 201
  108. theorem OAI.CycleClique.certificate_303_checked line 203
  109. theorem OAI.CycleClique.certificate_303_valid line 204
  110. def OAI.CycleClique.certificate_304_q line 206
  111. def OAI.CycleClique.certificate_304_edges line 207
  112. def OAI.CycleClique.certificate_304_part_0 line 209
  113. def OAI.CycleClique.certificate_304 line 211
  114. theorem OAI.CycleClique.certificate_304_checked line 213
  115. theorem OAI.CycleClique.certificate_304_valid line 214
  116. def OAI.CycleClique.certificate_305_q line 216
  117. def OAI.CycleClique.certificate_305_edges line 217
  118. def OAI.CycleClique.certificate_305_part_0 line 219
  119. def OAI.CycleClique.certificate_305_part_1 line 221
  120. def OAI.CycleClique.certificate_305 line 223
  121. theorem OAI.CycleClique.certificate_305_checked line 225
  122. theorem OAI.CycleClique.certificate_305_valid line 226
  123. def OAI.CycleClique.certificate_306_q line 228
  124. def OAI.CycleClique.certificate_306_edges line 229
  125. def OAI.CycleClique.certificate_306_part_0 line 231
  126. def OAI.CycleClique.certificate_306_part_1 line 233
  127. def OAI.CycleClique.certificate_306 line 235
  128. theorem OAI.CycleClique.certificate_306_checked line 237
  129. theorem OAI.CycleClique.certificate_306_valid line 238
  130. def OAI.CycleClique.certificate_307_q line 240
  131. def OAI.CycleClique.certificate_307_edges line 241
  132. def OAI.CycleClique.certificate_307_part_0 line 243
  133. def OAI.CycleClique.certificate_307_part_1 line 245
  134. def OAI.CycleClique.certificate_307 line 247
  135. theorem OAI.CycleClique.certificate_307_checked line 249
  136. theorem OAI.CycleClique.certificate_307_valid line 250
  137. def OAI.CycleClique.certificate_308_q line 252
  138. def OAI.CycleClique.certificate_308_edges line 253
  139. def OAI.CycleClique.certificate_308_part_0 line 255
  140. def OAI.CycleClique.certificate_308_part_1 line 257
  141. def OAI.CycleClique.certificate_308 line 259
  142. theorem OAI.CycleClique.certificate_308_checked line 261
  143. theorem OAI.CycleClique.certificate_308_valid line 262
  144. def OAI.CycleClique.certificate_309_q line 264
  145. def OAI.CycleClique.certificate_309_edges line 265
  146. def OAI.CycleClique.certificate_309_part_0 line 267
  147. def OAI.CycleClique.certificate_309_part_1 line 269
  148. def OAI.CycleClique.certificate_309 line 271
  149. theorem OAI.CycleClique.certificate_309_checked line 273
  150. theorem OAI.CycleClique.certificate_309_valid line 274
  151. def OAI.CycleClique.certificate_310_q line 276
  152. def OAI.CycleClique.certificate_310_edges line 277
  153. def OAI.CycleClique.certificate_310_part_0 line 279
  154. def OAI.CycleClique.certificate_310_part_1 line 281
  155. def OAI.CycleClique.certificate_310 line 283
  156. theorem OAI.CycleClique.certificate_310_checked line 285
  157. theorem OAI.CycleClique.certificate_310_valid line 286
  158. def OAI.CycleClique.certificate_311_q line 288
  159. def OAI.CycleClique.certificate_311_edges line 289
  160. def OAI.CycleClique.certificate_311_part_0 line 291
  161. def OAI.CycleClique.certificate_311_part_1 line 293
  162. def OAI.CycleClique.certificate_311 line 295
  163. theorem OAI.CycleClique.certificate_311_checked line 297
  164. theorem OAI.CycleClique.certificate_311_valid line 298
  165. def OAI.CycleClique.certificate_312_q line 300
  166. def OAI.CycleClique.certificate_312_edges line 301
  167. def OAI.CycleClique.certificate_312_part_0 line 303
  168. def OAI.CycleClique.certificate_312_part_1 line 305
  169. def OAI.CycleClique.certificate_312 line 307
  170. theorem OAI.CycleClique.certificate_312_checked line 309
  171. theorem OAI.CycleClique.certificate_312_valid line 310
  172. def OAI.CycleClique.certificate_313_q line 312
  173. def OAI.CycleClique.certificate_313_edges line 313
  174. def OAI.CycleClique.certificate_313_part_0 line 315
  175. def OAI.CycleClique.certificate_313_part_1 line 317
  176. def OAI.CycleClique.certificate_313 line 319
  177. theorem OAI.CycleClique.certificate_313_checked line 321
  178. theorem OAI.CycleClique.certificate_313_valid line 322
  179. def OAI.CycleClique.certificate_314_q line 324
  180. def OAI.CycleClique.certificate_314_edges line 325
  181. def OAI.CycleClique.certificate_314_part_0 line 327
  182. def OAI.CycleClique.certificate_314 line 329
  183. theorem OAI.CycleClique.certificate_314_checked line 331
  184. theorem OAI.CycleClique.certificate_314_valid line 332
  185. def OAI.CycleClique.certificate_315_q line 334
  186. def OAI.CycleClique.certificate_315_edges line 335
  187. def OAI.CycleClique.certificate_315_part_0 line 337
  188. def OAI.CycleClique.certificate_315_part_1 line 339
  189. def OAI.CycleClique.certificate_315 line 341
  190. theorem OAI.CycleClique.certificate_315_checked line 343
  191. theorem OAI.CycleClique.certificate_315_valid line 344
  192. def OAI.CycleClique.certificate_316_q line 346
  193. def OAI.CycleClique.certificate_316_edges line 347
  194. def OAI.CycleClique.certificate_316_part_0 line 349
  195. def OAI.CycleClique.certificate_316_part_1 line 351
  196. def OAI.CycleClique.certificate_316 line 353
  197. theorem OAI.CycleClique.certificate_316_checked line 355
  198. theorem OAI.CycleClique.certificate_316_valid line 356
  199. def OAI.CycleClique.certificate_317_q line 358
  200. def OAI.CycleClique.certificate_317_edges line 359
  201. def OAI.CycleClique.certificate_317_part_0 line 361
  202. def OAI.CycleClique.certificate_317_part_1 line 363
  203. def OAI.CycleClique.certificate_317 line 365
  204. theorem OAI.CycleClique.certificate_317_checked line 367
  205. theorem OAI.CycleClique.certificate_317_valid line 368
  206. def OAI.CycleClique.certificate_318_q line 370
  207. def OAI.CycleClique.certificate_318_edges line 371
  208. def OAI.CycleClique.certificate_318_part_0 line 373
  209. def OAI.CycleClique.certificate_318_part_1 line 375
  210. def OAI.CycleClique.certificate_318 line 377
  211. theorem OAI.CycleClique.certificate_318_checked line 379
  212. theorem OAI.CycleClique.certificate_318_valid line 380
  213. def OAI.CycleClique.certificate_319_q line 382
  214. def OAI.CycleClique.certificate_319_edges line 383
  215. def OAI.CycleClique.certificate_319_part_0 line 385
  216. def OAI.CycleClique.certificate_319_part_1 line 387
  217. def OAI.CycleClique.certificate_319 line 389
  218. theorem OAI.CycleClique.certificate_319_checked line 391
  219. theorem OAI.CycleClique.certificate_319_valid line 392