OAI/Combinatorics/Ramsey/CycleClique/CertificateModel.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.PackingValid line 18
  2. instance OAI.CycleClique.(instance at line 21) line 21
  3. theorem OAI.CycleClique.packing_impossible line 26
  4. inductive OAI.CycleClique.FiniteCertificate line 39
  5. def OAI.CycleClique.FiniteCertificate.Valid line 48
  6. instance OAI.CycleClique.FiniteCertificate.instDecidableValid line 58
  7. theorem OAI.CycleClique.FiniteCertificate.sound line 69
  8. def OAI.CycleClique.normalizedChain line 92
  9. theorem OAI.CycleClique.normalizedChain_cases line 94
  10. theorem OAI.CycleClique.normalizedChain_normal line 97
  11. def OAI.CycleClique.canonicalPattern line 104
  12. theorem OAI.CycleClique.canonicalPattern_sorted line 107
  13. theorem OAI.CycleClique.canonicalPattern_normal line 114
  14. theorem OAI.CycleClique.ClosedChain.reverse line 120
  15. theorem OAI.CycleClique.normalize_amounts line 129
  16. theorem OAI.CycleClique.PathSystem.canonical_realization line 151
  17. theorem OAI.CycleClique.PathSystem.optimal_of_same line 179
  18. def OAI.CycleClique.chainOrder line 188
  19. def OAI.CycleClique.chainClique line 190
  20. def OAI.CycleClique.patternChainsFrom line 194
  21. def OAI.CycleClique.patternCliqueFrom line 198
  22. def OAI.CycleClique.patternOrder line 202
  23. def OAI.CycleClique.patternClique line 204
  24. def OAI.CycleClique.patternEdges line 206
  25. def OAI.CycleClique.patternAmount line 210
  26. def OAI.CycleClique.patternSize line 212
  27. def OAI.CycleClique.patternEdgeCount line 214
  28. theorem OAI.CycleClique.patternOrder_nil line 216
  29. theorem OAI.CycleClique.patternOrder_cons line 217
  30. theorem OAI.CycleClique.patternChainsFrom_length line 220
  31. theorem OAI.CycleClique.patternChainsFrom_flatten line 226
  32. theorem OAI.CycleClique.patternOrder_eq line 234
  33. theorem OAI.CycleClique.chainClique_bounds line 242
  34. theorem OAI.CycleClique.patternCliqueFrom_bounds line 253
  35. theorem OAI.CycleClique.map_range_getD line 264
  36. theorem OAI.CycleClique.ChainAmounts.clique_map line 271
  37. theorem OAI.CycleClique.amounts_order line 298
  38. theorem OAI.CycleClique.amounts_shape line 306
  39. def OAI.CycleClique.PathSystem.labelState line 329
  40. theorem OAI.CycleClique.PathSystem.profile_parameters line 400
  41. def OAI.CycleClique.chainChoices line 414
  42. theorem OAI.CycleClique.mem_chainChoices line 419
  43. def OAI.CycleClique.patternChoices line 443
  44. theorem OAI.CycleClique.patternSize_cons line 452
  45. theorem OAI.CycleClique.patternAmount_cons line 456
  46. theorem OAI.CycleClique.mem_patternChoices line 460