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

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover6 line 8
2. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover5 line 12
3. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover7 line 18
4. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover8 line 22
5. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover9 line 26
6. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover10 line 30
7. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover11 line 34
8. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover4 line 38
9. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover12 line 63
10. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover13 line 69
11. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover14 line 73
12. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover15 line 77
13. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover16 line 81
14. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover17 line 85
15. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover18 line 91
16. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover19 line 95
17. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover20 line 99
18. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover21 line 105
19. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover22 line 111
20. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover3 line 117
21. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover24 line 192
22. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover25 line 196
23. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover26 line 200
24. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover27 line 204
25. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover23 line 208
26. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover28 line 230
27. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover29 line 236
28. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover30 line 240
29. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover31 line 244
30. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover32 line 248
31. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover33 line 254
32. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover34 line 258
33. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover35 line 262
34. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover36 line 268
35. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover37 line 272
36. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover39 line 278
37. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover40 line 282
38. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover38 line 286
39. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover41 line 305
40. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover42 line 309
41. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover43 line 315
42. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover44 line 321
43. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover45 line 337
44. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover46 line 350
45. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_seq2 line 360
46. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t4_cover1 line 507
47. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k9_t4 line 512
48. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover6 line 516
49. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover5 line 520
50. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover7 line 526
51. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover8 line 530
52. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover9 line 534
53. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover10 line 538
54. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover4 line 542
55. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover11 line 564
56. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover12 line 570
57. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover13 line 574
58. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover14 line 578
59. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover15 line 582
60. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover16 line 588
61. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover17 line 592
62. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover18 line 598
63. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover3 line 604
64. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover20 line 660
65. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover21 line 664
66. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover22 line 668
67. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover19 line 672
68. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover23 line 691
69. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover24 line 697
70. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover25 line 701
71. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover26 line 705
72. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover27 line 711
73. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover28 line 715
74. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover30 line 721
75. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover29 line 725
76. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover31 line 741
77. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover32 line 747
78. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover33 line 760
79. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover2 line 770
80. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover35 line 862
81. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover36 line 868
82. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover37 line 872
83. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover38 line 876
84. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover39 line 882
85. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover34 line 888
86. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover41 line 928
87. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover40 line 932
88. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover42 line 948
89. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover43 line 954
90. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover44 line 958
91. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover45 line 964
92. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover46 line 977
93. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover47 line 983
94. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover49 line 993
95. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover48 line 999
96. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover50 line 1026
97. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover51 line 1036
98. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover52 line 1053
99. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t5_cover1 line 1063
100. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k9_t5 line 1174
101. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover7 line 1178
102. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover6 line 1182
103. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover8 line 1188
104. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover9 line 1192
105. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover10 line 1196
106. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover5 line 1200
107. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover11 line 1219
108. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover12 line 1225
109. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover13 line 1229
110. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover14 line 1233
111. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover15 line 1239
112. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover4 line 1245
113. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover17 line 1285
114. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover18 line 1289
115. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover16 line 1293
116. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover19 line 1309
117. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover20 line 1315
118. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover21 line 1319
119. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover22 line 1325
120. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover23 line 1338
121. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover3 line 1348
122. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover25 line 1403
123. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover26 line 1409
124. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover27 line 1413
125. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover24 line 1419
126. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover28 line 1446
127. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover29 line 1459
128. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover30 line 1465
129. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover31 line 1475
130. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover32 line 1492
131. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover2 line 1502
132. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover35 line 1561
133. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover34 line 1565
134. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover36 line 1578
135. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover37 line 1584
136. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover33 line 1594
137. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover38 line 1625
138. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover39 line 1642
139. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover40 line 1652
140. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover41 line 1662
141. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover42 line 1679
142. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t6_cover1 line 1689
143. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k9_t6 line 1748
144. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover8 line 1752
145. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover7 line 1756
146. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover9 line 1762
147. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover10 line 1766
148. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover6 line 1770
149. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover11 line 1786
150. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover12 line 1792
151. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover13 line 1796
152. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover5 line 1802
153. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover15 line 1829
154. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover14 line 1833
155. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover16 line 1846
156. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover17 line 1852
157. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover4 line 1862
158. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover19 line 1893
159. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover18 line 1899
160. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover20 line 1916
161. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover21 line 1926
162. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover3 line 1936
163. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover23 line 1967
164. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover22 line 1977
165. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover24 line 1994
166. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover25 line 2004
167. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover2 line 2014
168. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover27 line 2045
169. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover26 line 2055
170. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover28 line 2072
171. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover29 line 2082
172. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t7_cover1 line 2092
173. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k9_t7 line 2123
174. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover9 line 2127
175. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover8 line 2131
176. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover10 line 2137
177. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover7 line 2141
178. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover11 line 2154
179. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover6 line 2160
180. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover12 line 2177
181. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover5 line 2187
182. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover13 line 2204
183. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover4 line 2214
184. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover14 line 2231
185. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover3 line 2241
186. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover15 line 2258
187. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover2 line 2268
188. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover16 line 2285
189. theorem OAI.CycleClique.Construction.CertifiedCoverage.k9t8_cover1 line 2295
190. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k9_t8 line 2312