OAI/Combinatorics/Ramsey/CycleClique/BallPacking.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.pathEdges line 15
  2. def OAI.CycleClique.pathLabels line 19
  3. def OAI.CycleClique.augmentedEdges line 21
  4. theorem OAI.CycleClique.pathEdges_mem line 24
  5. theorem OAI.CycleClique.pathLabels_bound line 37
  6. theorem OAI.CycleClique.pathEdges_sound line 48
  7. def OAI.CycleClique.LabelState.extendedFunction line 66
  8. theorem OAI.CycleClique.LabelState.extendedFunction_old line 69
  9. theorem OAI.CycleClique.LabelState.extendedFunction_new line 72
  10. theorem OAI.CycleClique.LabelState.extendedFunction_inj line 77
  11. theorem OAI.CycleClique.LabelState.extendedFunction_range' line 110
  12. theorem OAI.CycleClique.LabelState.exists_extension line 116
  13. def OAI.CycleClique.LabelCycleValid line 161
  14. instance OAI.CycleClique.(instance at line 164) line 164
  15. theorem OAI.CycleClique.cycle_of_list line 169
  16. theorem OAI.CycleClique.LabelState.cycle line 190
  17. structure OAI.CycleClique.OriginalSystem line 208
  18. def OAI.CycleClique.Improvement line 219
  19. instance OAI.CycleClique.(instance at line 225) line 225
  20. theorem OAI.CycleClique.OriginalSystem.impossible line 229
  21. theorem OAI.CycleClique.OutsidePath.restrict line 252
  22. theorem OAI.CycleClique.LabelState.forbidden_extension line 258
  23. abbrev OAI.CycleClique.ForbiddenMatrix line 272
  24. def OAI.CycleClique.matrixEntry line 274
  25. instance OAI.CycleClique.(instance at line 276) line 276
  26. structure OAI.CycleClique.ValidMatrix line 280
  27. theorem OAI.CycleClique.ValidMatrix.lookup line 292
  28. theorem OAI.CycleClique.ValidMatrix.extend line 299
  29. theorem OAI.CycleClique.ValidMatrix.insert line 308
  30. theorem OAI.CycleClique.OutsidePath.of_adj line 323
  31. def OAI.CycleClique.Excluded line 333
  32. instance OAI.CycleClique.(instance at line 336) line 336
  33. def OAI.CycleClique.LabelState.imageLabels line 345
  34. theorem OAI.CycleClique.LabelState.imageLabels_card line 347
  35. theorem OAI.CycleClique.LabelState.imageLabels_subset line 351
  36. theorem OAI.CycleClique.LabelState.excluded_notMem line 356
  37. theorem OAI.CycleClique.LabelState.excluded_zero line 361
  38. theorem OAI.CycleClique.LabelState.excluded_ball line 368
  39. inductive OAI.CycleClique.BallCertificate line 382
  40. def OAI.CycleClique.BallCertificate.radius line 388
  41. def OAI.CycleClique.BallCertificate.size line 392
  42. def OAI.CycleClique.BallCertificate.weight line 396
  43. def OAI.CycleClique.BallCertificate.Valid line 400
  44. instance OAI.CycleClique.BallCertificate.instDecidableValid line 408
  45. theorem OAI.CycleClique.BallCertificate.sound line 416
  46. inductive OAI.CycleClique.PackingOption line 457
  47. def OAI.CycleClique.PackingOption.base line 464
  48. def OAI.CycleClique.PackingOption.radiusCode line 467
  49. def OAI.CycleClique.PackingOption.weight line 471
  50. def OAI.CycleClique.PackingOption.Valid line 475
  51. instance OAI.CycleClique.PackingOption.(instance at line 478) line 478
  52. def OAI.CycleClique.PackingOption.Compatible line 482
  53. instance OAI.CycleClique.PackingOption.(instance at line 486) line 486
  54. def OAI.CycleClique.PackingOption.vertices line 490
  55. theorem OAI.CycleClique.PackingOption.weight_le line 494
  56. theorem OAI.CycleClique.PackingOption.separated line 503