OAI/Computability/BinPacking/Packing/CoordinateOrder.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.Geometry.posLT line 14
  2. def OAI.BinPackingGap.Geometry.posLE line 17
  3. theorem OAI.BinPackingGap.Geometry.posLT_irrefl line 19
  4. theorem OAI.BinPackingGap.Geometry.posLT_trans line 22
  5. theorem OAI.BinPackingGap.Geometry.posLT_asymm line 27
  6. theorem OAI.BinPackingGap.Geometry.posLT_trichotomy line 30
  7. theorem OAI.BinPackingGap.Geometry.posLT_or_posLT_of_ne line 35
  8. theorem OAI.BinPackingGap.Geometry.posLE_iff_not_posLT line 42
  9. theorem OAI.BinPackingGap.Geometry.posLE_refl line 46
  10. theorem OAI.BinPackingGap.Geometry.posLE_trans line 48
  11. theorem OAI.BinPackingGap.Geometry.heightCode_ge_theta line 56
  12. theorem OAI.BinPackingGap.Geometry.heightCode_le_edgeMax line 63
  13. theorem OAI.BinPackingGap.Geometry.heightCode_same_edge_sub line 72
  14. theorem OAI.BinPackingGap.Geometry.heightCode_next_rep_sub line 78
  15. theorem OAI.BinPackingGap.Geometry.heightCode_next_edge_sub line 86
  16. theorem OAI.BinPackingGap.Geometry.theta_next_sub line 95
  17. theorem OAI.BinPackingGap.Geometry.heightCode_jump line 101
  18. theorem OAI.BinPackingGap.Geometry.theta_jump line 119
  19. theorem OAI.BinPackingGap.Geometry.theta_jump_ge_heightCode line 127
  20. theorem OAI.BinPackingGap.Geometry.heightCode_strictMono line 132
  21. theorem OAI.BinPackingGap.Geometry.heightCode_lt_iff line 138
  22. theorem OAI.BinPackingGap.Geometry.baseline_gap_of_posLT line 149
  23. theorem OAI.BinPackingGap.Geometry.gap_le_abs_baseline_sub line 158
  24. theorem OAI.BinPackingGap.Geometry.baseline_lt_iff line 165
  25. theorem OAI.BinPackingGap.Geometry.baseline_le_iff line 181
  26. theorem OAI.BinPackingGap.Geometry.baseline_eq_iff line 192
  27. theorem OAI.BinPackingGap.Geometry.baseline_le_jobInterior_iff line 203
  28. theorem OAI.BinPackingGap.Geometry.jobInterior_lt_baseline_iff line 214
  29. theorem OAI.BinPackingGap.Geometry.jobInterior_mem_current line 220
  30. theorem OAI.BinPackingGap.Geometry.jobInterior_mem_job_iff line 225
  31. theorem OAI.BinPackingGap.Geometry.baseline_le_actualJobInterior_iff line 241
  32. theorem OAI.BinPackingGap.Geometry.actualJobInterior_mem_job_iff line 245