OAI/Combinatorics/Progressions/Estimates/ImageCosetReconstruction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.factorsThrough_target_cosets line 12
  2. theorem OAI.Erdos3.exists_unique_quotient_reconstruction line 33
  3. theorem OAI.Erdos3.exists_unique_observable_reconstruction line 49
  4. theorem OAI.Erdos3.exists_unique_image_reconstruction line 59
  5. def OAI.Erdos3.CosetImage line 85
  6. def OAI.Erdos3.projectToCosetImage line 88
  7. theorem OAI.Erdos3.projectToCosetImage_surjective line 91
  8. theorem OAI.Erdos3.factorsThrough_image_cosets line 96
  9. theorem OAI.Erdos3.exists_unique_cosetImage_reconstruction line 116