OAI/Combinatorics/Progressions/Sampling/RationalGridMajorSet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.rationalGridMajorSet line 11
2. theorem OAI.Erdos3.mem_rationalGridMajorSet line 16
3. theorem OAI.Erdos3.integerSymmetricInterval_card line 27
4. theorem OAI.Erdos3.rationalGridMajorSet_card line 32
5. def OAI.Erdos3.rationalGridMajorBox line 60
6. theorem OAI.Erdos3.rationalGridMajorBox_card line 64