OAI/Combinatorics/Progressions/Geometry/IntervalBoxDifference.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.SymmetricIntegerInterval line 12
  2. instance OAI.Erdos3.symmetricIntegerInterval_inhabited line 15
  3. theorem OAI.Erdos3.symmetricIntegerInterval_card line 18
  4. theorem OAI.Erdos3.symmetricIntegerInterval_abs_le line 22
  5. theorem OAI.Erdos3.dense_product_signed_box line 26
  6. def OAI.Erdos3.intervalDifference line 55
  7. theorem OAI.Erdos3.intervalDifference_injective line 58
  8. def OAI.Erdos3.intervalBoxDifference line 66
  9. theorem OAI.Erdos3.intervalBoxDifference_injective line 70
  10. theorem OAI.Erdos3.intervalBox_card_ratio line 76
  11. theorem OAI.Erdos3.nearIntegerDensity_interval_differences line 99