OAI/Computability/BinPacking/PCP/FiniteGraph.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectionCounts line 19
  2. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectionCounts_nonempty line 23
  3. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.minimumRejections line 28
  4. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.minimumRejections_le line 31
  5. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.exists_minimizer line 36
  6. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.le_minimumRejections_iff line 43
  7. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.minimumRejections_le_card line 53
  8. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectionCount_eq_zero_iff line 60
  9. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.minimumRejections_eq_zero_iff line 75
  10. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.gap line 85
  11. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.gap_nonnegative line 88
  12. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.gap_le_one line 91
  13. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.gap_eq_zero_iff line 97
  14. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.le_gap_iff line 103
  15. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.inverse_card_le_gap_of_unsatisfiable line 116
  16. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.reindex line 130
  17. def OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.labelingEquiv line 144
  18. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.reindex_edgeSatisfied line 150
  19. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.reindex_rejectionCount line 157
  20. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.rejectionCounts_reindex line 181
  21. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.minimumRejections_reindex line 198
  22. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.gap_reindex line 204
  23. theorem OAI.BinPackingGames.Foundations.PCP.ConstraintGraph.satisfiable_reindex line 210
  24. structure OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle line 220
  25. instance OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeVertex line 234
  26. instance OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeDart line 235
  27. instance OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqVertex line 236
  28. instance OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqDart line 237
  29. instance OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyDart line 238
  30. instance OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyVertex line 240
  31. def OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph line 244
  32. def OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.size line 256
  33. def OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.Satisfiable line 258
  34. def OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.rejectionCount line 260
  35. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.size_positive line 263
  36. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.dartCard_le_size line 266
  37. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_graph line 269
  38. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_size line 273
  39. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_satisfiable line 277
  40. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_rejectionCount line 281
  41. def OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.minimumRejections line 288
  42. def OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.gap line 290
  43. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.exists_minimizer line 292
  44. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.gap_nonnegative line 296
  45. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.gap_le_one line 298
  46. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.gap_eq_zero_iff line 300
  47. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.le_gap_iff line 303
  48. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.inverse_card_le_gap_of_unsatisfiable line 308
  49. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.one_le_dartCard_mul_gap line 312
  50. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.one_le_size_mul_gap line 318
  51. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_minimumRejections line 325
  52. theorem OAI.BinPackingGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_gap line 329