OAI/Computability/BinPacking/Packing/PackingSelections.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.PackingCounts.subclass line 18
  2. def OAI.BinPackingGap.PackingCounts.label line 21
  3. def OAI.BinPackingGap.PackingCounts.globalResources line 24
  4. theorem OAI.BinPackingGap.PackingCounts.globalCopy_injective line 29
  5. theorem OAI.BinPackingGap.PackingCounts.globalResources_card line 37
  6. theorem OAI.BinPackingGap.PackingCounts.mem_globalResources line 44
  7. theorem OAI.BinPackingGap.PackingCounts.globalResources_disjoint line 51
  8. def OAI.BinPackingGap.PackingCounts.fundedTuples line 64
  9. theorem OAI.BinPackingGap.PackingCounts.mem_fundedTuples line 70
  10. theorem OAI.BinPackingGap.PackingCounts.fundedTuples_subset_main line 78
  11. theorem OAI.BinPackingGap.PackingCounts.fundedTuples_disjoint_label line 84
  12. theorem OAI.BinPackingGap.PackingCounts.sum_card_main_subsets_le_resources line 90
  13. theorem OAI.BinPackingGap.PackingCounts.fundedTuples_sum_card_le line 111
  14. def OAI.BinPackingGap.PackingCounts.xplus line 120
  15. def OAI.BinPackingGap.PackingCounts.xminus line 123
  16. theorem OAI.BinPackingGap.PackingCounts.xplus_budget line 126
  17. theorem OAI.BinPackingGap.PackingCounts.xminus_budget line 130
  18. theorem OAI.BinPackingGap.PackingCounts.total_budget line 134
  19. def OAI.BinPackingGap.PackingCounts.localDepthResources line 144
  20. theorem OAI.BinPackingGap.PackingCounts.localDepthCopy_injective line 150
  21. theorem OAI.BinPackingGap.PackingCounts.localDepthResources_card line 161
  22. theorem OAI.BinPackingGap.PackingCounts.card_le_localDepth_stock line 169
  23. def OAI.BinPackingGap.PackingCounts.positiveLocalResources line 177
  24. theorem OAI.BinPackingGap.PackingCounts.mem_positiveLocalResources line 182
  25. theorem OAI.BinPackingGap.PackingCounts.positiveLocalCopy_injective line 189
  26. theorem OAI.BinPackingGap.PackingCounts.positiveLocalResources_card line 198
  27. theorem OAI.BinPackingGap.PackingCounts.card_le_positiveLocal_stock line 205
  28. def OAI.BinPackingGap.PackingCounts.elementAtRole line 223
  29. theorem OAI.BinPackingGap.PackingCounts.elementAtRole_mk line 226
  30. theorem OAI.BinPackingGap.PackingCounts.selected_role line 233
  31. def OAI.BinPackingGap.PackingCounts.roleCopy line 240
  32. theorem OAI.BinPackingGap.PackingCounts.roleCopy_item line 244
  33. theorem OAI.BinPackingGap.PackingCounts.roleCopy_injective line 249
  34. theorem OAI.BinPackingGap.PackingCounts.roleCopy_subclass line 257
  35. abbrev OAI.BinPackingGap.PackingCounts.rowCopy line 264
  36. abbrev OAI.BinPackingGap.PackingCounts.anchorCopy line 268
  37. abbrev OAI.BinPackingGap.PackingCounts.globalCopy line 272
  38. abbrev OAI.BinPackingGap.PackingCounts.localCopy line 276
  39. theorem OAI.BinPackingGap.PackingCounts.selected_global_resource_iff line 280
  40. theorem OAI.BinPackingGap.PackingCounts.selected_row_label line 301
  41. theorem OAI.BinPackingGap.PackingCounts.selected_anchor_label line 309
  42. theorem OAI.BinPackingGap.PackingCounts.selected_local_label line 317
  43. theorem OAI.BinPackingGap.PackingCounts.good_row_vertex line 325
  44. theorem OAI.BinPackingGap.PackingCounts.good_anchor_vertex line 334
  45. theorem OAI.BinPackingGap.PackingCounts.good_local_vertex line 342
  46. def OAI.BinPackingGap.PackingCounts.zeroPositiveTuples line 351
  47. def OAI.BinPackingGap.PackingCounts.tupleLocalDepth line 358
  48. theorem OAI.BinPackingGap.PackingCounts.mem_zeroPositiveTuples line 362
  49. theorem OAI.BinPackingGap.PackingCounts.zeroPositiveTuples_card_le line 371
  50. theorem OAI.BinPackingGap.PackingCounts.localCopy_eq_of_positive line 377
  51. theorem OAI.BinPackingGap.PackingCounts.selected_depth_mem line 390
  52. theorem OAI.BinPackingGap.PackingCounts.selected_localDepth_resource line 403
  53. theorem OAI.BinPackingGap.PackingCounts.zeroPositiveTuples_depth_card_le line 421