OAI/Combinatorics/Progressions/Estimates/FiniteAssignmentPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos3.MissingAssignment line 12
2. def OAI.Erdos3.assignmentSplitMap line 14
3. theorem OAI.Erdos3.assignmentSplitMap_bijective line 18
4. def OAI.Erdos3.assignmentSplitEquiv line 40
5. theorem OAI.Erdos3.missingAssignment_coordinate line 44
6. theorem OAI.Erdos3.assignmentSplit_card line 50
7. theorem OAI.Erdos3.assignment_product_split line 56