OAI/Combinatorics/Progressions/Sampling/NormalizedRealBoxHalfGrid.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.uniformIntervalGrid line 14
  2. theorem OAI.Erdos3.uniformIntervalGrid_mem line 17
  3. theorem OAI.Erdos3.exists_uniformIntervalGrid_approx line 31
  4. def OAI.Erdos3.uniformBoxGrid line 53
  5. theorem OAI.Erdos3.uniformBoxGrid_mem line 56
  6. theorem OAI.Erdos3.exists_uniformBoxGrid_approx line 60
  7. theorem OAI.Erdos3.uniformBoxGrid_card line 70
  8. def OAI.Erdos3.normalizedRealBoxGrid line 81
  9. theorem OAI.Erdos3.normalizedRealBoxGrid_bound line 85
  10. theorem OAI.Erdos3.exists_normalizedRealBoxGrid_cell line 93
  11. theorem OAI.Erdos3.exists_uniformIntervalGrid_half_approx line 125
  12. theorem OAI.Erdos3.exists_normalizedRealBoxGrid_half_cell line 155