OAI/NumberTheory/Jacobsthal/Partitions/BinCutGapMovement.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.GeometricBoxImages.geometricBoxes line 14
  2. theorem OAI.Erdos970.NumberTheoryLean.GeometricBoxImages.geometric_boxes_subset line 19
  3. theorem OAI.Erdos970.NumberTheoryLean.GeometricBoxImages.geometric_box_anchor line 26
  4. def OAI.Erdos970.NumberTheoryLean.BinCutSelections.aboveMultiplicity line 43
  5. def OAI.Erdos970.NumberTheoryLean.BinCutSelections.aboveSelection line 45
  6. def OAI.Erdos970.NumberTheoryLean.BinCutSelections.belowMultiplicity line 48
  7. def OAI.Erdos970.NumberTheoryLean.BinCutSelections.belowSelection line 50
  8. theorem OAI.Erdos970.NumberTheoryLean.BinCutSelections.above_selection_mem line 53
  9. theorem OAI.Erdos970.NumberTheoryLean.BinCutSelections.below_selection_mem line 61
  10. theorem OAI.Erdos970.NumberTheoryLean.BinCutSelections.above_word_membership line 69
  11. theorem OAI.Erdos970.NumberTheoryLean.BinCutSelections.below_word_membership line 85
  12. theorem OAI.Erdos970.NumberTheoryLean.SourceLabelStrictOrder.prime_lt_of_label_lt line 107
  13. def OAI.Erdos970.NumberTheoryLean.AssembleAtBin.assemble line 120
  14. theorem OAI.Erdos970.NumberTheoryLean.AssembleAtBin.above_zero_outside line 123
  15. theorem OAI.Erdos970.NumberTheoryLean.AssembleAtBin.assembled_mem line 129
  16. theorem OAI.Erdos970.NumberTheoryLean.AssembleAtBin.assembled_above line 142
  17. theorem OAI.Erdos970.NumberTheoryLean.AssembleAtBin.assembled_edge line 152
  18. theorem OAI.Erdos970.NumberTheoryLean.AssembleAtBin.assembled_below line 155
  19. theorem OAI.Erdos970.NumberTheoryLean.BinCutGapMovement.above_total_le line 170
  20. theorem OAI.Erdos970.NumberTheoryLean.BinCutGapMovement.above_word_length_le line 177
  21. theorem OAI.Erdos970.NumberTheoryLean.BinCutGapMovement.above_gap_movement line 184