OAI/Computability/BinPacking/Inventory/LabelConservation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.FinitePrefixConservation.remaining_eq_bad line 13
  2. theorem OAI.BinPackingGap.FinitePrefixConservation.remaining_le_bad line 23
  3. def OAI.BinPackingGap.LabelConservation.outsideItems line 45
  4. def OAI.BinPackingGap.LabelConservation.prefixItems line 47
  5. def OAI.BinPackingGap.LabelConservation.prefixOutside line 50
  6. def OAI.BinPackingGap.LabelConservation.exports line 53
  7. def OAI.BinPackingGap.LabelConservation.labelDefects line 58
  8. theorem OAI.BinPackingGap.LabelConservation.prefixItems_zero line 63
  9. theorem OAI.BinPackingGap.LabelConservation.prefixOutside_zero line 66
  10. theorem OAI.BinPackingGap.LabelConservation.exports_zero line 71
  11. theorem OAI.BinPackingGap.LabelConservation.prefix_inventory_eq line 76
  12. theorem OAI.BinPackingGap.LabelConservation.outside_add_selected_eq line 91
  13. theorem OAI.BinPackingGap.LabelConservation.selected_add_exports_eq line 108
  14. theorem OAI.BinPackingGap.LabelConservation.exports_add_outsideRole_eq_outsideAnchor line 128
  15. theorem OAI.BinPackingGap.LabelConservation.exports_eq_outside_sub line 143
  16. theorem OAI.BinPackingGap.LabelConservation.exports_card_le_outside line 156
  17. theorem OAI.BinPackingGap.LabelConservation.labelDefects_subset_exports line 171
  18. theorem OAI.BinPackingGap.LabelConservation.labelDefects_card_le_outside line 186
  19. def OAI.BinPackingGap.LabelConservation.badAnchors line 197
  20. theorem OAI.BinPackingGap.LabelConservation.mem_badAnchors_iff line 204
  21. theorem OAI.BinPackingGap.LabelConservation.badAnchors_card_le_three_mul line 250