OAI/Combinatorics/Progressions/Geometry/RelativePatchWholeBoxConclusion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos3.ResidueBoxSlice.wholeBox line 13
2. theorem OAI.Erdos3.ResidueBoxSlice.wholeBox_point line 18
3. theorem OAI.Erdos3.ResidueBoxSlice.wholeBox_integerPoint line 24
4. theorem OAI.Erdos3.ResidueBoxSlice.wholeBox_integerPoints line 31
5. theorem OAI.Erdos3.relativePatchSliceScore_wholeBox line 53
6. theorem OAI.Erdos3.relativePatchSliceConclusion_of_boxScore line 72
7. theorem OAI.Erdos3.relativePatchBoxScore_eq_subtype line 86
8. theorem OAI.Erdos3.relativePatchSliceConclusion_of_subtypeScore line 104