OAI/Computability/BinPacking/Packing/PackingFeasibility.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.PackingCounts.good_selected_labels line 15
  2. theorem OAI.BinPackingGap.PackingCounts.selected_itemCoordinate line 38
  3. theorem OAI.BinPackingGap.PackingCounts.good_coordinate_nonpos line 45
  4. theorem OAI.BinPackingGap.PackingCounts.main_anchor_of_subclass line 71
  5. theorem OAI.BinPackingGap.PackingCounts.globalCoordinate_of_not_w line 78
  6. theorem OAI.BinPackingGap.PackingCounts.main_anchor_copy line 87
  7. theorem OAI.BinPackingGap.PackingCounts.main_globalCoordinate line 94
  8. theorem OAI.BinPackingGap.PackingCounts.main_completion_le_deadline line 101
  9. theorem OAI.BinPackingGap.PackingCounts.main_completion_le_selected_deadline line 125
  10. theorem OAI.BinPackingGap.PackingCounts.job_row_of_subclass line 139
  11. theorem OAI.BinPackingGap.PackingCounts.key_anchor_of_subclass line 148
  12. theorem OAI.BinPackingGap.PackingCounts.edge_global_of_subclass line 155
  13. theorem OAI.BinPackingGap.PackingCounts.edge_local_of_subclass line 165
  14. structure OAI.BinPackingGap.PackingCounts.EdgeTupleData line 172
  15. theorem OAI.BinPackingGap.PackingCounts.edgeTupleData_nonempty line 186
  16. def OAI.BinPackingGap.PackingCounts.EdgeTupleData.expression line 207
  17. theorem OAI.BinPackingGap.PackingCounts.EdgeTupleData.expression_eq_coordinates line 211
  18. theorem OAI.BinPackingGap.PackingCounts.EdgeTupleData.feasible line 223
  19. theorem OAI.BinPackingGap.PackingCounts.EdgeTupleData.row_order line 231
  20. theorem OAI.BinPackingGap.PackingCounts.EdgeTupleData.edge_order line 235
  21. theorem OAI.BinPackingGap.PackingCounts.EdgeTupleData.exact_long_resource line 239
  22. theorem OAI.BinPackingGap.PackingCounts.edge_tuple_feasible line 252
  23. theorem OAI.BinPackingGap.PackingCounts.edge_selected_baseline_le line 266