OAI/Computability/BinPacking/Inventory/LocalCompletionCoverage.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.PartialAllocation.exists_equiv_extending_embeddings line 13
  2. theorem OAI.BinPackingGap.PartialAllocation.exists_equiv_extending_injections line 42
  3. theorem OAI.BinPackingGap.InventoryData.designated_injective line 57
  4. theorem OAI.BinPackingGap.InventoryData.deadline_undesignated line 62
  5. def OAI.BinPackingGap.InventoryData.deadlineShiftData line 77
  6. theorem OAI.BinPackingGap.InventoryData.deadline_prefix_active line 86
  7. theorem OAI.BinPackingGap.InventoryData.deadline_active_card line 93
  8. theorem OAI.BinPackingGap.InventoryData.deadline_prefix line 122
  9. theorem OAI.BinPackingGap.InventoryData.deadline_prefix_at_test line 131
  10. theorem OAI.BinPackingGap.InventoryData.exists_deadline_matching line 142
  11. def OAI.BinPackingGap.LocalResourceAllocation.oppositeTree line 167
  12. def OAI.BinPackingGap.LocalResourceAllocation.oppositeMarking line 171
  13. abbrev OAI.BinPackingGap.LocalResourceAllocation.OppositeMarked line 176
  14. theorem OAI.BinPackingGap.LocalResourceAllocation.opposite_height line 179
  15. theorem OAI.BinPackingGap.LocalResourceAllocation.opposite_depth_pos line 185
  16. theorem OAI.BinPackingGap.LocalResourceAllocation.opposite_quota line 191
  17. def OAI.BinPackingGap.LocalResourceAllocation.markedDepth line 203
  18. def OAI.BinPackingGap.LocalResourceAllocation.markedByDepth line 208
  19. def OAI.BinPackingGap.LocalResourceAllocation.markedResource line 218
  20. theorem OAI.BinPackingGap.LocalResourceAllocation.markedResource_depth line 227
  21. def OAI.BinPackingGap.LocalResourceAllocation.markedRow line 230
  22. theorem OAI.BinPackingGap.LocalResourceAllocation.markedRow_injective line 235
  23. theorem OAI.BinPackingGap.LocalResourceAllocation.fundedRoot_ne_markedRow line 245
  24. def OAI.BinPackingGap.LocalResourceAllocation.zeroResource line 250
  25. theorem OAI.BinPackingGap.LocalResourceAllocation.zeroResource_local_length line 260
  26. def OAI.BinPackingGap.LocalResourceAllocation.seedRows line 263
  27. def OAI.BinPackingGap.LocalResourceAllocation.seedResources line 273
  28. theorem OAI.BinPackingGap.LocalResourceAllocation.exists_localEquiv line 286
  29. def OAI.BinPackingGap.LocalResourceAllocation.localEquiv line 302
  30. theorem OAI.BinPackingGap.LocalResourceAllocation.localEquiv_seed line 305
  31. theorem OAI.BinPackingGap.LocalResourceAllocation.localEquiv_fundedRoot line 311
  32. theorem OAI.BinPackingGap.LocalResourceAllocation.localEquiv_markedRow line 316
  33. theorem OAI.BinPackingGap.LocalResourceAllocation.fundedRoot_local_zero line 322
  34. theorem OAI.BinPackingGap.LocalResourceAllocation.markedRow_local_length line 327
  35. theorem OAI.BinPackingGap.LocalResourceAllocation.plusMarked_local_length line 337
  36. theorem OAI.BinPackingGap.LocalResourceAllocation.minusMarked_local_length line 344
  37. theorem OAI.BinPackingGap.LocalCompletionCoverage.card_le_coverage line 357
  38. theorem OAI.BinPackingGap.LocalCompletionCoverage.nodeInterval_subset_root line 367
  39. def OAI.BinPackingGap.LocalCompletionCoverage.localCompletion line 387
  40. theorem OAI.BinPackingGap.LocalCompletionCoverage.localCompletion_le_baseline line 391
  41. theorem OAI.BinPackingGap.LocalCompletionCoverage.fundedRoot_covers line 409
  42. theorem OAI.BinPackingGap.LocalCompletionCoverage.fundedRoot_coverage line 422
  43. theorem OAI.BinPackingGap.LocalCompletionCoverage.plusMarked_completion_le line 432
  44. theorem OAI.BinPackingGap.LocalCompletionCoverage.minusMarked_completion_le line 458
  45. theorem OAI.BinPackingGap.LocalCompletionCoverage.plusMarked_coverage line 484
  46. theorem OAI.BinPackingGap.LocalCompletionCoverage.minusMarked_coverage line 501
  47. theorem OAI.BinPackingGap.LocalCompletionCoverage.shortJob_coverage line 518
  48. theorem OAI.BinPackingGap.LocalCompletionCoverage.localCompletion_coverage line 540
  49. theorem OAI.BinPackingGap.LocalCompletionCoverage.exists_anchorEquiv line 565