OAI/Computability/BinPacking/Inventory/PackingExclusions.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.excludedPositions line 14
  2. theorem OAI.BinPackingGap.mem_excludedPositions line 19
  3. theorem OAI.BinPackingGap.excludedPositions_card_le line 25
  4. def OAI.BinPackingGap.excludedRepetitions line 45
  5. def OAI.BinPackingGap.nonexcludedRepetitions line 50
  6. theorem OAI.BinPackingGap.mem_excludedRepetitions line 55
  7. theorem OAI.BinPackingGap.mem_nonexcludedRepetitions line 61
  8. theorem OAI.BinPackingGap.excludedRepetitions_card_le line 67
  9. theorem OAI.BinPackingGap.excluded_nonexcluded_card line 79
  10. theorem OAI.BinPackingGap.nonexcludedRepetitions_add_card_bound line 96
  11. theorem OAI.BinPackingGap.nonexcludedRepetitions_card_ge line 105
  12. theorem OAI.BinPackingGap.nonexcludedRepetitions_card_ge_real line 111
  13. theorem OAI.BinPackingGap.nonexcludedRepetitions_card_ge_of_unique_hits line 119
  14. theorem OAI.BinPackingGap.nonexcludedRepetitions_card_ge_real_of_unique_hits line 126
  15. def OAI.BinPackingGap.PackingCounts.tupleHitsJob line 138
  16. def OAI.BinPackingGap.PackingCounts.excludedAt line 143
  17. theorem OAI.BinPackingGap.PackingCounts.selected_hits_job_unique line 147
  18. theorem OAI.BinPackingGap.PackingCounts.excludedAt_card_le line 154
  19. def OAI.BinPackingGap.PackingCounts.goodRepetitions line 161
  20. theorem OAI.BinPackingGap.PackingCounts.goodRepetitions_card_ge line 165
  21. theorem OAI.BinPackingGap.PackingCounts.goodRepetitions_card_ge_real line 170
  22. theorem OAI.BinPackingGap.PackingCounts.covering_not_selected_of_nonexcluded line 175