OAI/Combinatorics/Progressions/Model.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.HasAP line 7

   Also declared: ComparatorChallenges/ErdosReciprocal.lean:7 (same declaration text).

2. def OAI.Erdos3.APFree line 10
3. def OAI.Erdos3.extremalNumber line 12
4. def OAI.Erdos3.reciprocalTerm line 23

   Also declared: ComparatorChallenges/ErdosReciprocal.lean:16 (same declaration text).

5. def OAI.Erdos3.QuantitativeDensityBound line 31
6. def OAI.Erdos3.QuantitativeDensityTheorem line 37
7. def OAI.Erdos3.ReciprocalProgressionTheorem line 40

   Also declared: ComparatorChallenges/ErdosReciprocal.lean:24 (same declaration text).