OAI/Combinatorics/Ramsey/CycleClique/Certificates015.lean

GitHub source file

251 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_448_q line 20
  2. def OAI.CycleClique.certificate_448_edges line 21
  3. def OAI.CycleClique.certificate_448_part_0 line 23
  4. def OAI.CycleClique.certificate_448_part_1 line 25
  5. def OAI.CycleClique.certificate_448 line 27
  6. theorem OAI.CycleClique.certificate_448_checked line 29
  7. theorem OAI.CycleClique.certificate_448_valid line 30
  8. def OAI.CycleClique.certificate_449_q line 32
  9. def OAI.CycleClique.certificate_449_edges line 33
  10. def OAI.CycleClique.certificate_449_part_0 line 35
  11. def OAI.CycleClique.certificate_449_part_1 line 37
  12. def OAI.CycleClique.certificate_449 line 39
  13. theorem OAI.CycleClique.certificate_449_checked line 41
  14. theorem OAI.CycleClique.certificate_449_valid line 42
  15. def OAI.CycleClique.certificate_450_q line 44
  16. def OAI.CycleClique.certificate_450_edges line 45
  17. def OAI.CycleClique.certificate_450_part_0 line 47
  18. def OAI.CycleClique.certificate_450_part_1 line 49
  19. def OAI.CycleClique.certificate_450 line 51
  20. theorem OAI.CycleClique.certificate_450_checked line 53
  21. theorem OAI.CycleClique.certificate_450_valid line 54
  22. def OAI.CycleClique.certificate_451_q line 56
  23. def OAI.CycleClique.certificate_451_edges line 57
  24. def OAI.CycleClique.certificate_451_part_0 line 59
  25. def OAI.CycleClique.certificate_451_part_1 line 61
  26. def OAI.CycleClique.certificate_451_part_2 line 63
  27. def OAI.CycleClique.certificate_451 line 65
  28. theorem OAI.CycleClique.certificate_451_checked line 67
  29. theorem OAI.CycleClique.certificate_451_valid line 68
  30. def OAI.CycleClique.certificate_452_q line 70
  31. def OAI.CycleClique.certificate_452_edges line 71
  32. def OAI.CycleClique.certificate_452_part_0 line 73
  33. def OAI.CycleClique.certificate_452_part_1 line 75
  34. def OAI.CycleClique.certificate_452_part_2 line 77
  35. def OAI.CycleClique.certificate_452 line 79
  36. theorem OAI.CycleClique.certificate_452_checked line 81
  37. theorem OAI.CycleClique.certificate_452_valid line 82
  38. def OAI.CycleClique.certificate_453_q line 84
  39. def OAI.CycleClique.certificate_453_edges line 85
  40. def OAI.CycleClique.certificate_453_part_0 line 87
  41. def OAI.CycleClique.certificate_453_part_1 line 89
  42. def OAI.CycleClique.certificate_453_part_2 line 91
  43. def OAI.CycleClique.certificate_453 line 93
  44. theorem OAI.CycleClique.certificate_453_checked line 95
  45. theorem OAI.CycleClique.certificate_453_valid line 96
  46. def OAI.CycleClique.certificate_454_q line 98
  47. def OAI.CycleClique.certificate_454_edges line 99
  48. def OAI.CycleClique.certificate_454_part_0 line 101
  49. def OAI.CycleClique.certificate_454_part_1 line 103
  50. def OAI.CycleClique.certificate_454 line 105
  51. theorem OAI.CycleClique.certificate_454_checked line 107
  52. theorem OAI.CycleClique.certificate_454_valid line 108
  53. def OAI.CycleClique.certificate_455_q line 110
  54. def OAI.CycleClique.certificate_455_edges line 111
  55. def OAI.CycleClique.certificate_455_part_0 line 113
  56. def OAI.CycleClique.certificate_455_part_1 line 115
  57. def OAI.CycleClique.certificate_455_part_2 line 117
  58. def OAI.CycleClique.certificate_455 line 119
  59. theorem OAI.CycleClique.certificate_455_checked line 121
  60. theorem OAI.CycleClique.certificate_455_valid line 122
  61. def OAI.CycleClique.certificate_456_q line 124
  62. def OAI.CycleClique.certificate_456_edges line 125
  63. def OAI.CycleClique.certificate_456_part_0 line 127
  64. def OAI.CycleClique.certificate_456_part_1 line 129
  65. def OAI.CycleClique.certificate_456_part_2 line 131
  66. def OAI.CycleClique.certificate_456 line 133
  67. theorem OAI.CycleClique.certificate_456_checked line 135
  68. theorem OAI.CycleClique.certificate_456_valid line 136
  69. def OAI.CycleClique.certificate_457_q line 138
  70. def OAI.CycleClique.certificate_457_edges line 139
  71. def OAI.CycleClique.certificate_457_part_0 line 141
  72. def OAI.CycleClique.certificate_457_part_1 line 143
  73. def OAI.CycleClique.certificate_457_part_2 line 145
  74. def OAI.CycleClique.certificate_457 line 147
  75. theorem OAI.CycleClique.certificate_457_checked line 149
  76. theorem OAI.CycleClique.certificate_457_valid line 150
  77. def OAI.CycleClique.certificate_458_q line 152
  78. def OAI.CycleClique.certificate_458_edges line 153
  79. def OAI.CycleClique.certificate_458_part_0 line 155
  80. def OAI.CycleClique.certificate_458_part_1 line 157
  81. def OAI.CycleClique.certificate_458_part_2 line 159
  82. def OAI.CycleClique.certificate_458 line 161
  83. theorem OAI.CycleClique.certificate_458_checked line 163
  84. theorem OAI.CycleClique.certificate_458_valid line 164
  85. def OAI.CycleClique.certificate_459_q line 166
  86. def OAI.CycleClique.certificate_459_edges line 167
  87. def OAI.CycleClique.certificate_459_part_0 line 169
  88. def OAI.CycleClique.certificate_459_part_1 line 171
  89. def OAI.CycleClique.certificate_459_part_2 line 173
  90. def OAI.CycleClique.certificate_459 line 175
  91. theorem OAI.CycleClique.certificate_459_checked line 177
  92. theorem OAI.CycleClique.certificate_459_valid line 178
  93. def OAI.CycleClique.certificate_460_q line 180
  94. def OAI.CycleClique.certificate_460_edges line 181
  95. def OAI.CycleClique.certificate_460_part_0 line 183
  96. def OAI.CycleClique.certificate_460_part_1 line 185
  97. def OAI.CycleClique.certificate_460 line 187
  98. theorem OAI.CycleClique.certificate_460_checked line 189
  99. theorem OAI.CycleClique.certificate_460_valid line 190
  100. def OAI.CycleClique.certificate_461_q line 192
  101. def OAI.CycleClique.certificate_461_edges line 193
  102. def OAI.CycleClique.certificate_461_part_0 line 195
  103. def OAI.CycleClique.certificate_461_part_1 line 197
  104. def OAI.CycleClique.certificate_461_part_2 line 199
  105. def OAI.CycleClique.certificate_461 line 201
  106. theorem OAI.CycleClique.certificate_461_checked line 203
  107. theorem OAI.CycleClique.certificate_461_valid line 204
  108. def OAI.CycleClique.certificate_462_q line 206
  109. def OAI.CycleClique.certificate_462_edges line 207
  110. def OAI.CycleClique.certificate_462_part_0 line 209
  111. def OAI.CycleClique.certificate_462_part_1 line 211
  112. def OAI.CycleClique.certificate_462_part_2 line 213
  113. def OAI.CycleClique.certificate_462 line 215
  114. theorem OAI.CycleClique.certificate_462_checked line 217
  115. theorem OAI.CycleClique.certificate_462_valid line 218
  116. def OAI.CycleClique.certificate_463_q line 220
  117. def OAI.CycleClique.certificate_463_edges line 221
  118. def OAI.CycleClique.certificate_463_part_0 line 223
  119. def OAI.CycleClique.certificate_463_part_1 line 225
  120. def OAI.CycleClique.certificate_463_part_2 line 227
  121. def OAI.CycleClique.certificate_463 line 229
  122. theorem OAI.CycleClique.certificate_463_checked line 231
  123. theorem OAI.CycleClique.certificate_463_valid line 232
  124. def OAI.CycleClique.certificate_464_q line 234
  125. def OAI.CycleClique.certificate_464_edges line 235
  126. def OAI.CycleClique.certificate_464_part_0 line 237
  127. def OAI.CycleClique.certificate_464_part_1 line 239
  128. def OAI.CycleClique.certificate_464_part_2 line 241
  129. def OAI.CycleClique.certificate_464 line 243
  130. theorem OAI.CycleClique.certificate_464_checked line 245
  131. theorem OAI.CycleClique.certificate_464_valid line 246
  132. def OAI.CycleClique.certificate_465_q line 248
  133. def OAI.CycleClique.certificate_465_edges line 249
  134. def OAI.CycleClique.certificate_465_part_0 line 251
  135. def OAI.CycleClique.certificate_465_part_1 line 253
  136. def OAI.CycleClique.certificate_465_part_2 line 255
  137. def OAI.CycleClique.certificate_465 line 257
  138. theorem OAI.CycleClique.certificate_465_checked line 259
  139. theorem OAI.CycleClique.certificate_465_valid line 260
  140. def OAI.CycleClique.certificate_466_q line 262
  141. def OAI.CycleClique.certificate_466_edges line 263
  142. def OAI.CycleClique.certificate_466_part_0 line 265
  143. def OAI.CycleClique.certificate_466_part_1 line 267
  144. def OAI.CycleClique.certificate_466_part_2 line 269
  145. def OAI.CycleClique.certificate_466 line 271
  146. theorem OAI.CycleClique.certificate_466_checked line 273
  147. theorem OAI.CycleClique.certificate_466_valid line 274
  148. def OAI.CycleClique.certificate_467_q line 276
  149. def OAI.CycleClique.certificate_467_edges line 277
  150. def OAI.CycleClique.certificate_467_part_0 line 279
  151. def OAI.CycleClique.certificate_467_part_1 line 281
  152. def OAI.CycleClique.certificate_467_part_2 line 283
  153. def OAI.CycleClique.certificate_467 line 285
  154. theorem OAI.CycleClique.certificate_467_checked line 287
  155. theorem OAI.CycleClique.certificate_467_valid line 288
  156. def OAI.CycleClique.certificate_468_q line 290
  157. def OAI.CycleClique.certificate_468_edges line 291
  158. def OAI.CycleClique.certificate_468_part_0 line 293
  159. def OAI.CycleClique.certificate_468_part_1 line 295
  160. def OAI.CycleClique.certificate_468_part_2 line 297
  161. def OAI.CycleClique.certificate_468 line 299
  162. theorem OAI.CycleClique.certificate_468_checked line 301
  163. theorem OAI.CycleClique.certificate_468_valid line 302
  164. def OAI.CycleClique.certificate_469_q line 304
  165. def OAI.CycleClique.certificate_469_edges line 305
  166. def OAI.CycleClique.certificate_469_part_0 line 307
  167. def OAI.CycleClique.certificate_469_part_1 line 309
  168. def OAI.CycleClique.certificate_469_part_2 line 311
  169. def OAI.CycleClique.certificate_469 line 313
  170. theorem OAI.CycleClique.certificate_469_checked line 315
  171. theorem OAI.CycleClique.certificate_469_valid line 316
  172. def OAI.CycleClique.certificate_470_q line 318
  173. def OAI.CycleClique.certificate_470_edges line 319
  174. def OAI.CycleClique.certificate_470_part_0 line 321
  175. def OAI.CycleClique.certificate_470_part_1 line 323
  176. def OAI.CycleClique.certificate_470_part_2 line 325
  177. def OAI.CycleClique.certificate_470 line 327
  178. theorem OAI.CycleClique.certificate_470_checked line 329
  179. theorem OAI.CycleClique.certificate_470_valid line 330
  180. def OAI.CycleClique.certificate_471_q line 332
  181. def OAI.CycleClique.certificate_471_edges line 333
  182. def OAI.CycleClique.certificate_471_part_0 line 335
  183. def OAI.CycleClique.certificate_471_part_1 line 337
  184. def OAI.CycleClique.certificate_471_part_2 line 339
  185. def OAI.CycleClique.certificate_471 line 341
  186. theorem OAI.CycleClique.certificate_471_checked line 343
  187. theorem OAI.CycleClique.certificate_471_valid line 344
  188. def OAI.CycleClique.certificate_472_q line 346
  189. def OAI.CycleClique.certificate_472_edges line 347
  190. def OAI.CycleClique.certificate_472_part_0 line 349
  191. def OAI.CycleClique.certificate_472_part_1 line 351
  192. def OAI.CycleClique.certificate_472_part_2 line 353
  193. def OAI.CycleClique.certificate_472 line 355
  194. theorem OAI.CycleClique.certificate_472_checked line 357
  195. theorem OAI.CycleClique.certificate_472_valid line 358
  196. def OAI.CycleClique.certificate_473_q line 360
  197. def OAI.CycleClique.certificate_473_edges line 361
  198. def OAI.CycleClique.certificate_473_part_0 line 363
  199. def OAI.CycleClique.certificate_473_part_1 line 365
  200. def OAI.CycleClique.certificate_473_part_2 line 367
  201. def OAI.CycleClique.certificate_473 line 369
  202. theorem OAI.CycleClique.certificate_473_checked line 371
  203. theorem OAI.CycleClique.certificate_473_valid line 372
  204. def OAI.CycleClique.certificate_474_q line 374
  205. def OAI.CycleClique.certificate_474_edges line 375
  206. def OAI.CycleClique.certificate_474_part_0 line 377
  207. def OAI.CycleClique.certificate_474_part_1 line 379
  208. def OAI.CycleClique.certificate_474_part_2 line 381
  209. def OAI.CycleClique.certificate_474 line 383
  210. theorem OAI.CycleClique.certificate_474_checked line 385
  211. theorem OAI.CycleClique.certificate_474_valid line 386
  212. def OAI.CycleClique.certificate_475_q line 388
  213. def OAI.CycleClique.certificate_475_edges line 389
  214. def OAI.CycleClique.certificate_475_part_0 line 391
  215. def OAI.CycleClique.certificate_475_part_1 line 393
  216. def OAI.CycleClique.certificate_475_part_2 line 395
  217. def OAI.CycleClique.certificate_475 line 397
  218. theorem OAI.CycleClique.certificate_475_checked line 399
  219. theorem OAI.CycleClique.certificate_475_valid line 400
  220. def OAI.CycleClique.certificate_476_q line 402
  221. def OAI.CycleClique.certificate_476_edges line 403
  222. def OAI.CycleClique.certificate_476_part_0 line 405
  223. def OAI.CycleClique.certificate_476_part_1 line 407
  224. def OAI.CycleClique.certificate_476_part_2 line 409
  225. def OAI.CycleClique.certificate_476 line 411
  226. theorem OAI.CycleClique.certificate_476_checked line 413
  227. theorem OAI.CycleClique.certificate_476_valid line 414
  228. def OAI.CycleClique.certificate_477_q line 416
  229. def OAI.CycleClique.certificate_477_edges line 417
  230. def OAI.CycleClique.certificate_477_part_0 line 419
  231. def OAI.CycleClique.certificate_477_part_1 line 421
  232. def OAI.CycleClique.certificate_477_part_2 line 423
  233. def OAI.CycleClique.certificate_477 line 425
  234. theorem OAI.CycleClique.certificate_477_checked line 427
  235. theorem OAI.CycleClique.certificate_477_valid line 428
  236. def OAI.CycleClique.certificate_478_q line 430
  237. def OAI.CycleClique.certificate_478_edges line 431
  238. def OAI.CycleClique.certificate_478_part_0 line 433
  239. def OAI.CycleClique.certificate_478_part_1 line 435
  240. def OAI.CycleClique.certificate_478_part_2 line 437
  241. def OAI.CycleClique.certificate_478 line 439
  242. theorem OAI.CycleClique.certificate_478_checked line 441
  243. theorem OAI.CycleClique.certificate_478_valid line 442
  244. def OAI.CycleClique.certificate_479_q line 444
  245. def OAI.CycleClique.certificate_479_edges line 445
  246. def OAI.CycleClique.certificate_479_part_0 line 447
  247. def OAI.CycleClique.certificate_479_part_1 line 449
  248. def OAI.CycleClique.certificate_479_part_2 line 451
  249. def OAI.CycleClique.certificate_479 line 453
  250. theorem OAI.CycleClique.certificate_479_checked line 455
  251. theorem OAI.CycleClique.certificate_479_valid line 456