OAI/Combinatorics/Progressions/Lattices/NearIntegerMultiples.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NearInteger line 12
  2. def OAI.Erdos3.nearIntegerDensity line 14
  3. theorem OAI.Erdos3.nearIntegerDensity_eq_card line 17
  4. theorem OAI.Erdos3.nearIntegerDensity_le_one line 22
  5. theorem OAI.Erdos3.card_div_le_nearIntegerDensity line 28
  6. theorem OAI.Erdos3.exists_constant_denominator_fiber line 36
  7. theorem OAI.Erdos3.nearIntegerDensity_product line 63
  8. theorem OAI.Erdos3.nearIntegerDensity_of_geometric_mean line 70
  9. theorem OAI.Erdos3.nearIntegerDensity_comp_injective line 99
  10. theorem OAI.Erdos3.nearIntegerDensity_fiber_injections line 117
  11. theorem OAI.Erdos3.nearInteger_multiples line 141