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

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover4 line 8
  2. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover3 line 12
  3. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover5 line 18
  4. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover6 line 22
  5. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover7 line 26
  6. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover8 line 30
  7. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover2 line 34
  8. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover9 line 56
  9. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover10 line 62
  10. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover11 line 66
  11. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover12 line 70
  12. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover13 line 74
  13. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover14 line 80
  14. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover15 line 84
  15. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover16 line 90
  16. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t3_cover1 line 96
  17. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k7_t3 line 152
  18. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover5 line 156
  19. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover4 line 160
  20. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover6 line 166
  21. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover7 line 170
  22. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover8 line 174
  23. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover3 line 178
  24. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover9 line 197
  25. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover10 line 203
  26. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover11 line 207
  27. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover12 line 211
  28. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover13 line 217
  29. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover2 line 223
  30. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover15 line 263
  31. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover16 line 267
  32. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover14 line 271
  33. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover17 line 287
  34. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover18 line 293
  35. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover19 line 297
  36. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover20 line 303
  37. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover21 line 316
  38. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t4_cover1 line 326
  39. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k7_t4 line 381
  40. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover6 line 385
  41. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover5 line 389
  42. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover7 line 395
  43. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover8 line 399
  44. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover4 line 403
  45. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover9 line 419
  46. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover10 line 425
  47. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover11 line 429
  48. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover3 line 435
  49. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover13 line 462
  50. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover12 line 466
  51. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover14 line 479
  52. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover15 line 485
  53. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover2 line 495
  54. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover17 line 526
  55. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover16 line 532
  56. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover18 line 549
  57. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover19 line 559
  58. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t5_cover1 line 569
  59. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k7_t5 line 600
  60. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover7 line 604
  61. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover6 line 608
  62. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover8 line 614
  63. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover5 line 618
  64. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover9 line 631
  65. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover4 line 637
  66. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover10 line 654
  67. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover3 line 664
  68. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover11 line 681
  69. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover2 line 691
  70. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover12 line 708
  71. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t6_cover1 line 718
  72. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k7_t6 line 735
  73. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover8 line 739
  74. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover7 line 743
  75. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover6 line 749
  76. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover5 line 759
  77. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover4 line 769
  78. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover3 line 779
  79. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover2 line 789
  80. theorem OAI.CycleClique.Construction.CertifiedCoverage.k7t7_cover1 line 799
  81. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k7_t7 line 809