OAI/Combinatorics/Ramsey/CycleClique/Certificates007.lean

GitHub source file

221 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_192_q line 20
  2. def OAI.CycleClique.certificate_192_edges line 21
  3. def OAI.CycleClique.certificate_192_part_0 line 23
  4. def OAI.CycleClique.certificate_192_part_1 line 25
  5. def OAI.CycleClique.certificate_192 line 27
  6. theorem OAI.CycleClique.certificate_192_checked line 29
  7. theorem OAI.CycleClique.certificate_192_valid line 30
  8. def OAI.CycleClique.certificate_193_q line 32
  9. def OAI.CycleClique.certificate_193_edges line 33
  10. def OAI.CycleClique.certificate_193_part_0 line 35
  11. def OAI.CycleClique.certificate_193_part_1 line 37
  12. def OAI.CycleClique.certificate_193 line 39
  13. theorem OAI.CycleClique.certificate_193_checked line 41
  14. theorem OAI.CycleClique.certificate_193_valid line 42
  15. def OAI.CycleClique.certificate_194_q line 44
  16. def OAI.CycleClique.certificate_194_edges line 45
  17. def OAI.CycleClique.certificate_194_part_0 line 47
  18. def OAI.CycleClique.certificate_194_part_1 line 49
  19. def OAI.CycleClique.certificate_194 line 51
  20. theorem OAI.CycleClique.certificate_194_checked line 53
  21. theorem OAI.CycleClique.certificate_194_valid line 54
  22. def OAI.CycleClique.certificate_195_q line 56
  23. def OAI.CycleClique.certificate_195_edges line 57
  24. def OAI.CycleClique.certificate_195_part_0 line 59
  25. def OAI.CycleClique.certificate_195_part_1 line 61
  26. def OAI.CycleClique.certificate_195 line 63
  27. theorem OAI.CycleClique.certificate_195_checked line 65
  28. theorem OAI.CycleClique.certificate_195_valid line 66
  29. def OAI.CycleClique.certificate_196_q line 68
  30. def OAI.CycleClique.certificate_196_edges line 69
  31. def OAI.CycleClique.certificate_196_part_0 line 71
  32. def OAI.CycleClique.certificate_196_part_1 line 73
  33. def OAI.CycleClique.certificate_196 line 75
  34. theorem OAI.CycleClique.certificate_196_checked line 77
  35. theorem OAI.CycleClique.certificate_196_valid line 78
  36. def OAI.CycleClique.certificate_197_q line 80
  37. def OAI.CycleClique.certificate_197_edges line 81
  38. def OAI.CycleClique.certificate_197_part_0 line 83
  39. def OAI.CycleClique.certificate_197_part_1 line 85
  40. def OAI.CycleClique.certificate_197 line 87
  41. theorem OAI.CycleClique.certificate_197_checked line 89
  42. theorem OAI.CycleClique.certificate_197_valid line 90
  43. def OAI.CycleClique.certificate_198_q line 92
  44. def OAI.CycleClique.certificate_198_edges line 93
  45. def OAI.CycleClique.certificate_198_part_0 line 95
  46. def OAI.CycleClique.certificate_198_part_1 line 97
  47. def OAI.CycleClique.certificate_198 line 99
  48. theorem OAI.CycleClique.certificate_198_checked line 101
  49. theorem OAI.CycleClique.certificate_198_valid line 102
  50. def OAI.CycleClique.certificate_199_q line 104
  51. def OAI.CycleClique.certificate_199_edges line 105
  52. def OAI.CycleClique.certificate_199_part_0 line 107
  53. def OAI.CycleClique.certificate_199_part_1 line 109
  54. def OAI.CycleClique.certificate_199 line 111
  55. theorem OAI.CycleClique.certificate_199_checked line 113
  56. theorem OAI.CycleClique.certificate_199_valid line 114
  57. def OAI.CycleClique.certificate_200_q line 116
  58. def OAI.CycleClique.certificate_200_edges line 117
  59. def OAI.CycleClique.certificate_200_part_0 line 119
  60. def OAI.CycleClique.certificate_200_part_1 line 121
  61. def OAI.CycleClique.certificate_200 line 123
  62. theorem OAI.CycleClique.certificate_200_checked line 125
  63. theorem OAI.CycleClique.certificate_200_valid line 126
  64. def OAI.CycleClique.certificate_201_q line 128
  65. def OAI.CycleClique.certificate_201_edges line 129
  66. def OAI.CycleClique.certificate_201_part_0 line 131
  67. def OAI.CycleClique.certificate_201_part_1 line 133
  68. def OAI.CycleClique.certificate_201 line 135
  69. theorem OAI.CycleClique.certificate_201_checked line 137
  70. theorem OAI.CycleClique.certificate_201_valid line 138
  71. def OAI.CycleClique.certificate_202_q line 140
  72. def OAI.CycleClique.certificate_202_edges line 141
  73. def OAI.CycleClique.certificate_202_part_0 line 143
  74. def OAI.CycleClique.certificate_202_part_1 line 145
  75. def OAI.CycleClique.certificate_202 line 147
  76. theorem OAI.CycleClique.certificate_202_checked line 149
  77. theorem OAI.CycleClique.certificate_202_valid line 150
  78. def OAI.CycleClique.certificate_203_q line 152
  79. def OAI.CycleClique.certificate_203_edges line 153
  80. def OAI.CycleClique.certificate_203_part_0 line 155
  81. def OAI.CycleClique.certificate_203 line 157
  82. theorem OAI.CycleClique.certificate_203_checked line 159
  83. theorem OAI.CycleClique.certificate_203_valid line 160
  84. def OAI.CycleClique.certificate_204_q line 162
  85. def OAI.CycleClique.certificate_204_edges line 163
  86. def OAI.CycleClique.certificate_204_part_0 line 165
  87. def OAI.CycleClique.certificate_204_part_1 line 167
  88. def OAI.CycleClique.certificate_204 line 169
  89. theorem OAI.CycleClique.certificate_204_checked line 171
  90. theorem OAI.CycleClique.certificate_204_valid line 172
  91. def OAI.CycleClique.certificate_205_q line 174
  92. def OAI.CycleClique.certificate_205_edges line 175
  93. def OAI.CycleClique.certificate_205_part_0 line 177
  94. def OAI.CycleClique.certificate_205_part_1 line 179
  95. def OAI.CycleClique.certificate_205 line 181
  96. theorem OAI.CycleClique.certificate_205_checked line 183
  97. theorem OAI.CycleClique.certificate_205_valid line 184
  98. def OAI.CycleClique.certificate_206_q line 186
  99. def OAI.CycleClique.certificate_206_edges line 187
  100. def OAI.CycleClique.certificate_206_part_0 line 189
  101. def OAI.CycleClique.certificate_206_part_1 line 191
  102. def OAI.CycleClique.certificate_206 line 193
  103. theorem OAI.CycleClique.certificate_206_checked line 195
  104. theorem OAI.CycleClique.certificate_206_valid line 196
  105. def OAI.CycleClique.certificate_207_q line 198
  106. def OAI.CycleClique.certificate_207_edges line 199
  107. def OAI.CycleClique.certificate_207_part_0 line 201
  108. def OAI.CycleClique.certificate_207_part_1 line 203
  109. def OAI.CycleClique.certificate_207 line 205
  110. theorem OAI.CycleClique.certificate_207_checked line 207
  111. theorem OAI.CycleClique.certificate_207_valid line 208
  112. def OAI.CycleClique.certificate_208_q line 210
  113. def OAI.CycleClique.certificate_208_edges line 211
  114. def OAI.CycleClique.certificate_208_part_0 line 213
  115. def OAI.CycleClique.certificate_208_part_1 line 215
  116. def OAI.CycleClique.certificate_208 line 217
  117. theorem OAI.CycleClique.certificate_208_checked line 219
  118. theorem OAI.CycleClique.certificate_208_valid line 220
  119. def OAI.CycleClique.certificate_209_q line 222
  120. def OAI.CycleClique.certificate_209_edges line 223
  121. def OAI.CycleClique.certificate_209_part_0 line 225
  122. def OAI.CycleClique.certificate_209_part_1 line 227
  123. def OAI.CycleClique.certificate_209 line 229
  124. theorem OAI.CycleClique.certificate_209_checked line 231
  125. theorem OAI.CycleClique.certificate_209_valid line 232
  126. def OAI.CycleClique.certificate_210_q line 234
  127. def OAI.CycleClique.certificate_210_edges line 235
  128. def OAI.CycleClique.certificate_210_part_0 line 237
  129. def OAI.CycleClique.certificate_210_part_1 line 239
  130. def OAI.CycleClique.certificate_210 line 241
  131. theorem OAI.CycleClique.certificate_210_checked line 243
  132. theorem OAI.CycleClique.certificate_210_valid line 244
  133. def OAI.CycleClique.certificate_211_q line 246
  134. def OAI.CycleClique.certificate_211_edges line 247
  135. def OAI.CycleClique.certificate_211_part_0 line 249
  136. def OAI.CycleClique.certificate_211_part_1 line 251
  137. def OAI.CycleClique.certificate_211 line 253
  138. theorem OAI.CycleClique.certificate_211_checked line 255
  139. theorem OAI.CycleClique.certificate_211_valid line 256
  140. def OAI.CycleClique.certificate_212_q line 258
  141. def OAI.CycleClique.certificate_212_edges line 259
  142. def OAI.CycleClique.certificate_212_part_0 line 261
  143. def OAI.CycleClique.certificate_212_part_1 line 263
  144. def OAI.CycleClique.certificate_212 line 265
  145. theorem OAI.CycleClique.certificate_212_checked line 267
  146. theorem OAI.CycleClique.certificate_212_valid line 268
  147. def OAI.CycleClique.certificate_213_q line 270
  148. def OAI.CycleClique.certificate_213_edges line 271
  149. def OAI.CycleClique.certificate_213_part_0 line 273
  150. def OAI.CycleClique.certificate_213_part_1 line 275
  151. def OAI.CycleClique.certificate_213 line 277
  152. theorem OAI.CycleClique.certificate_213_checked line 279
  153. theorem OAI.CycleClique.certificate_213_valid line 280
  154. def OAI.CycleClique.certificate_214_q line 282
  155. def OAI.CycleClique.certificate_214_edges line 283
  156. def OAI.CycleClique.certificate_214_part_0 line 285
  157. def OAI.CycleClique.certificate_214_part_1 line 287
  158. def OAI.CycleClique.certificate_214 line 289
  159. theorem OAI.CycleClique.certificate_214_checked line 291
  160. theorem OAI.CycleClique.certificate_214_valid line 292
  161. def OAI.CycleClique.certificate_215_q line 294
  162. def OAI.CycleClique.certificate_215_edges line 295
  163. def OAI.CycleClique.certificate_215_part_0 line 297
  164. def OAI.CycleClique.certificate_215_part_1 line 299
  165. def OAI.CycleClique.certificate_215 line 301
  166. theorem OAI.CycleClique.certificate_215_checked line 303
  167. theorem OAI.CycleClique.certificate_215_valid line 304
  168. def OAI.CycleClique.certificate_216_q line 306
  169. def OAI.CycleClique.certificate_216_edges line 307
  170. def OAI.CycleClique.certificate_216_part_0 line 309
  171. def OAI.CycleClique.certificate_216_part_1 line 311
  172. def OAI.CycleClique.certificate_216_part_2 line 313
  173. def OAI.CycleClique.certificate_216 line 315
  174. theorem OAI.CycleClique.certificate_216_checked line 317
  175. theorem OAI.CycleClique.certificate_216_valid line 318
  176. def OAI.CycleClique.certificate_217_q line 320
  177. def OAI.CycleClique.certificate_217_edges line 321
  178. def OAI.CycleClique.certificate_217_part_0 line 323
  179. def OAI.CycleClique.certificate_217_part_1 line 325
  180. def OAI.CycleClique.certificate_217_part_2 line 327
  181. def OAI.CycleClique.certificate_217 line 329
  182. theorem OAI.CycleClique.certificate_217_checked line 331
  183. theorem OAI.CycleClique.certificate_217_valid line 332
  184. def OAI.CycleClique.certificate_218_q line 334
  185. def OAI.CycleClique.certificate_218_edges line 335
  186. def OAI.CycleClique.certificate_218_part_0 line 337
  187. def OAI.CycleClique.certificate_218_part_1 line 339
  188. def OAI.CycleClique.certificate_218_part_2 line 341
  189. def OAI.CycleClique.certificate_218 line 343
  190. theorem OAI.CycleClique.certificate_218_checked line 345
  191. theorem OAI.CycleClique.certificate_218_valid line 346
  192. def OAI.CycleClique.certificate_219_q line 348
  193. def OAI.CycleClique.certificate_219_edges line 349
  194. def OAI.CycleClique.certificate_219_part_0 line 351
  195. def OAI.CycleClique.certificate_219 line 353
  196. theorem OAI.CycleClique.certificate_219_checked line 355
  197. theorem OAI.CycleClique.certificate_219_valid line 356
  198. def OAI.CycleClique.certificate_220_q line 358
  199. def OAI.CycleClique.certificate_220_edges line 359
  200. def OAI.CycleClique.certificate_220_part_0 line 361
  201. def OAI.CycleClique.certificate_220 line 363
  202. theorem OAI.CycleClique.certificate_220_checked line 365
  203. theorem OAI.CycleClique.certificate_220_valid line 366
  204. def OAI.CycleClique.certificate_221_q line 368
  205. def OAI.CycleClique.certificate_221_edges line 369
  206. def OAI.CycleClique.certificate_221_part_0 line 371
  207. def OAI.CycleClique.certificate_221 line 373
  208. theorem OAI.CycleClique.certificate_221_checked line 375
  209. theorem OAI.CycleClique.certificate_221_valid line 376
  210. def OAI.CycleClique.certificate_222_q line 378
  211. def OAI.CycleClique.certificate_222_edges line 379
  212. def OAI.CycleClique.certificate_222_part_0 line 381
  213. def OAI.CycleClique.certificate_222 line 383
  214. theorem OAI.CycleClique.certificate_222_checked line 385
  215. theorem OAI.CycleClique.certificate_222_valid line 386
  216. def OAI.CycleClique.certificate_223_q line 388
  217. def OAI.CycleClique.certificate_223_edges line 389
  218. def OAI.CycleClique.certificate_223_part_0 line 391
  219. def OAI.CycleClique.certificate_223 line 393
  220. theorem OAI.CycleClique.certificate_223_checked line 395
  221. theorem OAI.CycleClique.certificate_223_valid line 396