OAI/Combinatorics/Progressions/Geometry/DenseRealBoxCell.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FreimanModel.card_image_eq_of_same_fibers line 12
  2. theorem OAI.Erdos3.FreimanModel.card_difference_image_of_freiman line 37
  3. theorem OAI.Erdos3.FreimanModel.exists_nonempty_large_fiber line 67
  4. def OAI.Erdos3.realBoxCellCount line 98
  5. theorem OAI.Erdos3.realBoxCellCount_pos line 100
  6. theorem OAI.Erdos3.realBoxCellCount_le line 104
  7. theorem OAI.Erdos3.realBoxCell_floor_lt line 110
  8. def OAI.Erdos3.realBoxCellCenter line 117
  9. theorem OAI.Erdos3.realBoxCell_offset line 120
  10. theorem OAI.Erdos3.exists_dense_real_box_cell line 139