OAI/Computability/BinPacking/Trees/InventoryRowGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGap.InventoryData.node_right_in_root line 9
2. theorem OAI.BinPackingGap.InventoryData.rowBaseline_le_one_of_not_tm line 18
3. theorem OAI.BinPackingGap.InventoryData.rowBaseline_ge_four_of_tm line 28
4. theorem OAI.BinPackingGap.InventoryData.rowShort_eq_false_of_tm line 37
5. theorem OAI.BinPackingGap.InventoryData.exists_jobCopy_of_rowShort line 43
6. theorem OAI.BinPackingGap.InventoryData.row_zero_resources_empty line 51
7. theorem OAI.BinPackingGap.InventoryData.row_zero_resources_job line 58
8. theorem OAI.BinPackingGap.InventoryData.minus_row_completion_gt_one line 70
9. theorem OAI.BinPackingGap.InventoryData.minus_row_not_cover_jobInterior line 81
10. theorem OAI.BinPackingGap.InventoryData.plus_row_not_cover_minus_side line 94