OAI/Combinatorics/Ramsey/CycleClique/Certificates011.lean

GitHub source file

222 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_320_q line 20
  2. def OAI.CycleClique.certificate_320_edges line 21
  3. def OAI.CycleClique.certificate_320_part_0 line 23
  4. def OAI.CycleClique.certificate_320_part_1 line 25
  5. def OAI.CycleClique.certificate_320 line 27
  6. theorem OAI.CycleClique.certificate_320_checked line 29
  7. theorem OAI.CycleClique.certificate_320_valid line 30
  8. def OAI.CycleClique.certificate_321_q line 32
  9. def OAI.CycleClique.certificate_321_edges line 33
  10. def OAI.CycleClique.certificate_321_part_0 line 35
  11. def OAI.CycleClique.certificate_321_part_1 line 37
  12. def OAI.CycleClique.certificate_321 line 39
  13. theorem OAI.CycleClique.certificate_321_checked line 41
  14. theorem OAI.CycleClique.certificate_321_valid line 42
  15. def OAI.CycleClique.certificate_322_q line 44
  16. def OAI.CycleClique.certificate_322_edges line 45
  17. def OAI.CycleClique.certificate_322_part_0 line 47
  18. def OAI.CycleClique.certificate_322_part_1 line 49
  19. def OAI.CycleClique.certificate_322 line 51
  20. theorem OAI.CycleClique.certificate_322_checked line 53
  21. theorem OAI.CycleClique.certificate_322_valid line 54
  22. def OAI.CycleClique.certificate_323_q line 56
  23. def OAI.CycleClique.certificate_323_edges line 57
  24. def OAI.CycleClique.certificate_323_part_0 line 59
  25. def OAI.CycleClique.certificate_323_part_1 line 61
  26. def OAI.CycleClique.certificate_323 line 63
  27. theorem OAI.CycleClique.certificate_323_checked line 65
  28. theorem OAI.CycleClique.certificate_323_valid line 66
  29. def OAI.CycleClique.certificate_324_q line 68
  30. def OAI.CycleClique.certificate_324_edges line 69
  31. def OAI.CycleClique.certificate_324_part_0 line 71
  32. def OAI.CycleClique.certificate_324_part_1 line 73
  33. def OAI.CycleClique.certificate_324 line 75
  34. theorem OAI.CycleClique.certificate_324_checked line 77
  35. theorem OAI.CycleClique.certificate_324_valid line 78
  36. def OAI.CycleClique.certificate_325_q line 80
  37. def OAI.CycleClique.certificate_325_edges line 81
  38. def OAI.CycleClique.certificate_325_part_0 line 83
  39. def OAI.CycleClique.certificate_325 line 85
  40. theorem OAI.CycleClique.certificate_325_checked line 87
  41. theorem OAI.CycleClique.certificate_325_valid line 88
  42. def OAI.CycleClique.certificate_326_q line 90
  43. def OAI.CycleClique.certificate_326_edges line 91
  44. def OAI.CycleClique.certificate_326_part_0 line 93
  45. def OAI.CycleClique.certificate_326 line 95
  46. theorem OAI.CycleClique.certificate_326_checked line 97
  47. theorem OAI.CycleClique.certificate_326_valid line 98
  48. def OAI.CycleClique.certificate_327_q line 100
  49. def OAI.CycleClique.certificate_327_edges line 101
  50. def OAI.CycleClique.certificate_327_part_0 line 103
  51. def OAI.CycleClique.certificate_327_part_1 line 105
  52. def OAI.CycleClique.certificate_327 line 107
  53. theorem OAI.CycleClique.certificate_327_checked line 109
  54. theorem OAI.CycleClique.certificate_327_valid line 110
  55. def OAI.CycleClique.certificate_328_q line 112
  56. def OAI.CycleClique.certificate_328_edges line 113
  57. def OAI.CycleClique.certificate_328_part_0 line 115
  58. def OAI.CycleClique.certificate_328_part_1 line 117
  59. def OAI.CycleClique.certificate_328 line 119
  60. theorem OAI.CycleClique.certificate_328_checked line 121
  61. theorem OAI.CycleClique.certificate_328_valid line 122
  62. def OAI.CycleClique.certificate_329_q line 124
  63. def OAI.CycleClique.certificate_329_edges line 125
  64. def OAI.CycleClique.certificate_329_part_0 line 127
  65. def OAI.CycleClique.certificate_329_part_1 line 129
  66. def OAI.CycleClique.certificate_329 line 131
  67. theorem OAI.CycleClique.certificate_329_checked line 133
  68. theorem OAI.CycleClique.certificate_329_valid line 134
  69. def OAI.CycleClique.certificate_330_q line 136
  70. def OAI.CycleClique.certificate_330_edges line 137
  71. def OAI.CycleClique.certificate_330_part_0 line 139
  72. def OAI.CycleClique.certificate_330_part_1 line 141
  73. def OAI.CycleClique.certificate_330 line 143
  74. theorem OAI.CycleClique.certificate_330_checked line 145
  75. theorem OAI.CycleClique.certificate_330_valid line 146
  76. def OAI.CycleClique.certificate_331_q line 148
  77. def OAI.CycleClique.certificate_331_edges line 149
  78. def OAI.CycleClique.certificate_331_part_0 line 151
  79. def OAI.CycleClique.certificate_331_part_1 line 153
  80. def OAI.CycleClique.certificate_331 line 155
  81. theorem OAI.CycleClique.certificate_331_checked line 157
  82. theorem OAI.CycleClique.certificate_331_valid line 158
  83. def OAI.CycleClique.certificate_332_q line 160
  84. def OAI.CycleClique.certificate_332_edges line 161
  85. def OAI.CycleClique.certificate_332_part_0 line 163
  86. def OAI.CycleClique.certificate_332_part_1 line 165
  87. def OAI.CycleClique.certificate_332 line 167
  88. theorem OAI.CycleClique.certificate_332_checked line 169
  89. theorem OAI.CycleClique.certificate_332_valid line 170
  90. def OAI.CycleClique.certificate_333_q line 172
  91. def OAI.CycleClique.certificate_333_edges line 173
  92. def OAI.CycleClique.certificate_333_part_0 line 175
  93. def OAI.CycleClique.certificate_333_part_1 line 177
  94. def OAI.CycleClique.certificate_333 line 179
  95. theorem OAI.CycleClique.certificate_333_checked line 181
  96. theorem OAI.CycleClique.certificate_333_valid line 182
  97. def OAI.CycleClique.certificate_334_q line 184
  98. def OAI.CycleClique.certificate_334_edges line 185
  99. def OAI.CycleClique.certificate_334_part_0 line 187
  100. def OAI.CycleClique.certificate_334_part_1 line 189
  101. def OAI.CycleClique.certificate_334 line 191
  102. theorem OAI.CycleClique.certificate_334_checked line 193
  103. theorem OAI.CycleClique.certificate_334_valid line 194
  104. def OAI.CycleClique.certificate_335_q line 196
  105. def OAI.CycleClique.certificate_335_edges line 197
  106. def OAI.CycleClique.certificate_335_part_0 line 199
  107. def OAI.CycleClique.certificate_335_part_1 line 201
  108. def OAI.CycleClique.certificate_335 line 203
  109. theorem OAI.CycleClique.certificate_335_checked line 205
  110. theorem OAI.CycleClique.certificate_335_valid line 206
  111. def OAI.CycleClique.certificate_336_q line 208
  112. def OAI.CycleClique.certificate_336_edges line 209
  113. def OAI.CycleClique.certificate_336_part_0 line 211
  114. def OAI.CycleClique.certificate_336_part_1 line 213
  115. def OAI.CycleClique.certificate_336 line 215
  116. theorem OAI.CycleClique.certificate_336_checked line 217
  117. theorem OAI.CycleClique.certificate_336_valid line 218
  118. def OAI.CycleClique.certificate_337_q line 220
  119. def OAI.CycleClique.certificate_337_edges line 221
  120. def OAI.CycleClique.certificate_337_part_0 line 223
  121. def OAI.CycleClique.certificate_337_part_1 line 225
  122. def OAI.CycleClique.certificate_337 line 227
  123. theorem OAI.CycleClique.certificate_337_checked line 229
  124. theorem OAI.CycleClique.certificate_337_valid line 230
  125. def OAI.CycleClique.certificate_338_q line 232
  126. def OAI.CycleClique.certificate_338_edges line 233
  127. def OAI.CycleClique.certificate_338_part_0 line 235
  128. def OAI.CycleClique.certificate_338_part_1 line 237
  129. def OAI.CycleClique.certificate_338 line 239
  130. theorem OAI.CycleClique.certificate_338_checked line 241
  131. theorem OAI.CycleClique.certificate_338_valid line 242
  132. def OAI.CycleClique.certificate_339_q line 244
  133. def OAI.CycleClique.certificate_339_edges line 245
  134. def OAI.CycleClique.certificate_339_part_0 line 247
  135. def OAI.CycleClique.certificate_339_part_1 line 249
  136. def OAI.CycleClique.certificate_339 line 251
  137. theorem OAI.CycleClique.certificate_339_checked line 253
  138. theorem OAI.CycleClique.certificate_339_valid line 254
  139. def OAI.CycleClique.certificate_340_q line 256
  140. def OAI.CycleClique.certificate_340_edges line 257
  141. def OAI.CycleClique.certificate_340_part_0 line 259
  142. def OAI.CycleClique.certificate_340_part_1 line 261
  143. def OAI.CycleClique.certificate_340 line 263
  144. theorem OAI.CycleClique.certificate_340_checked line 265
  145. theorem OAI.CycleClique.certificate_340_valid line 266
  146. def OAI.CycleClique.certificate_341_q line 268
  147. def OAI.CycleClique.certificate_341_edges line 269
  148. def OAI.CycleClique.certificate_341_part_0 line 271
  149. def OAI.CycleClique.certificate_341_part_1 line 273
  150. def OAI.CycleClique.certificate_341 line 275
  151. theorem OAI.CycleClique.certificate_341_checked line 277
  152. theorem OAI.CycleClique.certificate_341_valid line 278
  153. def OAI.CycleClique.certificate_342_q line 280
  154. def OAI.CycleClique.certificate_342_edges line 281
  155. def OAI.CycleClique.certificate_342_part_0 line 283
  156. def OAI.CycleClique.certificate_342_part_1 line 285
  157. def OAI.CycleClique.certificate_342 line 287
  158. theorem OAI.CycleClique.certificate_342_checked line 289
  159. theorem OAI.CycleClique.certificate_342_valid line 290
  160. def OAI.CycleClique.certificate_343_q line 292
  161. def OAI.CycleClique.certificate_343_edges line 293
  162. def OAI.CycleClique.certificate_343_part_0 line 295
  163. def OAI.CycleClique.certificate_343_part_1 line 297
  164. def OAI.CycleClique.certificate_343 line 299
  165. theorem OAI.CycleClique.certificate_343_checked line 301
  166. theorem OAI.CycleClique.certificate_343_valid line 302
  167. def OAI.CycleClique.certificate_344_q line 304
  168. def OAI.CycleClique.certificate_344_edges line 305
  169. def OAI.CycleClique.certificate_344_part_0 line 307
  170. def OAI.CycleClique.certificate_344_part_1 line 309
  171. def OAI.CycleClique.certificate_344 line 311
  172. theorem OAI.CycleClique.certificate_344_checked line 313
  173. theorem OAI.CycleClique.certificate_344_valid line 314
  174. def OAI.CycleClique.certificate_345_q line 316
  175. def OAI.CycleClique.certificate_345_edges line 317
  176. def OAI.CycleClique.certificate_345_part_0 line 319
  177. def OAI.CycleClique.certificate_345_part_1 line 321
  178. def OAI.CycleClique.certificate_345 line 323
  179. theorem OAI.CycleClique.certificate_345_checked line 325
  180. theorem OAI.CycleClique.certificate_345_valid line 326
  181. def OAI.CycleClique.certificate_346_q line 328
  182. def OAI.CycleClique.certificate_346_edges line 329
  183. def OAI.CycleClique.certificate_346_part_0 line 331
  184. def OAI.CycleClique.certificate_346_part_1 line 333
  185. def OAI.CycleClique.certificate_346 line 335
  186. theorem OAI.CycleClique.certificate_346_checked line 337
  187. theorem OAI.CycleClique.certificate_346_valid line 338
  188. def OAI.CycleClique.certificate_347_q line 340
  189. def OAI.CycleClique.certificate_347_edges line 341
  190. def OAI.CycleClique.certificate_347_part_0 line 343
  191. def OAI.CycleClique.certificate_347_part_1 line 345
  192. def OAI.CycleClique.certificate_347 line 347
  193. theorem OAI.CycleClique.certificate_347_checked line 349
  194. theorem OAI.CycleClique.certificate_347_valid line 350
  195. def OAI.CycleClique.certificate_348_q line 352
  196. def OAI.CycleClique.certificate_348_edges line 353
  197. def OAI.CycleClique.certificate_348_part_0 line 355
  198. def OAI.CycleClique.certificate_348_part_1 line 357
  199. def OAI.CycleClique.certificate_348 line 359
  200. theorem OAI.CycleClique.certificate_348_checked line 361
  201. theorem OAI.CycleClique.certificate_348_valid line 362
  202. def OAI.CycleClique.certificate_349_q line 364
  203. def OAI.CycleClique.certificate_349_edges line 365
  204. def OAI.CycleClique.certificate_349_part_0 line 367
  205. def OAI.CycleClique.certificate_349_part_1 line 369
  206. def OAI.CycleClique.certificate_349 line 371
  207. theorem OAI.CycleClique.certificate_349_checked line 373
  208. theorem OAI.CycleClique.certificate_349_valid line 374
  209. def OAI.CycleClique.certificate_350_q line 376
  210. def OAI.CycleClique.certificate_350_edges line 377
  211. def OAI.CycleClique.certificate_350_part_0 line 379
  212. def OAI.CycleClique.certificate_350_part_1 line 381
  213. def OAI.CycleClique.certificate_350 line 383
  214. theorem OAI.CycleClique.certificate_350_checked line 385
  215. theorem OAI.CycleClique.certificate_350_valid line 386
  216. def OAI.CycleClique.certificate_351_q line 388
  217. def OAI.CycleClique.certificate_351_edges line 389
  218. def OAI.CycleClique.certificate_351_part_0 line 391
  219. def OAI.CycleClique.certificate_351_part_1 line 393
  220. def OAI.CycleClique.certificate_351 line 395
  221. theorem OAI.CycleClique.certificate_351_checked line 397
  222. theorem OAI.CycleClique.certificate_351_valid line 398