OAI/Computability/BinPacking/Inventory/InventoryCoverage.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.InventoryCoverage.itemRowBaseline line 14
  2. def OAI.BinPackingGap.InventoryCoverage.itemRowShort line 18
  3. def OAI.BinPackingGap.InventoryCoverage.itemKeyBaseline line 22
  4. def OAI.BinPackingGap.InventoryCoverage.itemDeadline line 26
  5. def OAI.BinPackingGap.InventoryCoverage.rowBaseline line 30
  6. def OAI.BinPackingGap.InventoryCoverage.rowShort line 32
  7. def OAI.BinPackingGap.InventoryCoverage.keyBaseline line 34
  8. def OAI.BinPackingGap.InventoryCoverage.anchorDeadline line 36
  9. theorem OAI.BinPackingGap.InventoryCoverage.rowBaseline_selected line 38
  10. theorem OAI.BinPackingGap.InventoryCoverage.rowShort_selected line 47
  11. theorem OAI.BinPackingGap.InventoryCoverage.keyBaseline_selected_of_key line 56
  12. theorem OAI.BinPackingGap.InventoryCoverage.anchorDeadline_selected_of_deadline line 66
  13. theorem OAI.BinPackingGap.InventoryCoverage.rowShort_implies_job line 75
  14. theorem OAI.BinPackingGap.InventoryCoverage.treeSubclass_ne_s line 91
  15. theorem OAI.BinPackingGap.InventoryCoverage.treeSubclass_tree line 94
  16. def OAI.BinPackingGap.InventoryCoverage.treePrefix line 101
  17. def OAI.BinPackingGap.InventoryCoverage.jobPrefix line 104
  18. def OAI.BinPackingGap.InventoryCoverage.originalBaselinePrefix line 107
  19. def OAI.BinPackingGap.InventoryCoverage.jobsAt line 110
  20. theorem OAI.BinPackingGap.InventoryCoverage.card_filter_transport line 114
  21. theorem OAI.BinPackingGap.InventoryCoverage.jobRowPrefix_card line 120
  22. theorem OAI.BinPackingGap.InventoryCoverage.treeRowPrefix_card line 133
  23. theorem OAI.BinPackingGap.InventoryCoverage.keyPrefix_card line 146
  24. theorem OAI.BinPackingGap.InventoryCoverage.deadlinePrefix_card line 159
  25. theorem OAI.BinPackingGap.InventoryCoverage.originalBaselinePrefix_card line 173
  26. theorem OAI.BinPackingGap.InventoryCoverage.currentKeyItems_card line 185
  27. theorem OAI.BinPackingGap.InventoryCoverage.currentShortItems_card line 198
  28. def OAI.BinPackingGap.InventoryCoverage.positionOf line 212
  29. theorem OAI.BinPackingGap.InventoryCoverage.positionOf_injective line 215
  30. theorem OAI.BinPackingGap.InventoryCoverage.job_baseline_eq_iff line 219
  31. theorem OAI.BinPackingGap.InventoryCoverage.jobsAt_position_card line 227
  32. theorem OAI.BinPackingGap.InventoryCoverage.actual_displaced_baseline_prefix_le line 240
  33. theorem OAI.BinPackingGap.InventoryCoverage.exists_job_of_subclass_s line 261
  34. theorem OAI.BinPackingGap.InventoryCoverage.row_before_current_le_interior line 276
  35. theorem OAI.BinPackingGap.InventoryCoverage.actual_displaced_job_prefix_le line 293
  36. theorem OAI.BinPackingGap.InventoryCoverage.actual_deadline_deficit_bound line 330
  37. theorem OAI.BinPackingGap.InventoryCoverage.actual_current_long_matches_from_correction line 357