OAI/Computability/BinPacking/Trees/KeyGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.Geometry.keyExpression line 9
  2. theorem OAI.BinPackingGap.Geometry.keyExpression_eq_coordinates line 14
  3. theorem OAI.BinPackingGap.Geometry.key_perturbation_lower line 22
  4. theorem OAI.BinPackingGap.Geometry.keyExpression_pos_of_later_row line 28
  5. theorem OAI.BinPackingGap.Geometry.keyExpression_pos_of_later_edge line 40
  6. theorem OAI.BinPackingGap.Geometry.row_order_of_key_feasible line 53
  7. theorem OAI.BinPackingGap.Geometry.edge_order_of_key_feasible line 61
  8. theorem OAI.BinPackingGap.Geometry.keyExpression_exact_position_edge line 69
  9. theorem OAI.BinPackingGap.Geometry.short_exact_key_feasible line 75
  10. theorem OAI.BinPackingGap.Geometry.long_exact_key_feasible_iff line 82
  11. theorem OAI.BinPackingGap.Geometry.exact_long_key_resource line 89