OAI/Combinatorics/Progressions/Geometry/RelativePatchBoxRestriction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.relativeBoxInput line 10
2. theorem OAI.Erdos3.relativeBoxInput_eq line 14
3. theorem OAI.Erdos3.relativeBoxInput_unitInterval line 19
4. theorem OAI.Erdos3.relativeBoxInput_signed_norm line 29
5. theorem OAI.Erdos3.relativeBoxInput_progressionFree line 38
6. theorem OAI.Erdos3.relativePatchBoxScore_congr_input line 50
7. theorem OAI.Erdos3.relativePatchSliceScore_congr_input line 58
8. theorem OAI.Erdos3.RelativePatchSliceConclusion.congr_input line 71