OAI/Combinatorics/Ryser/Selection/ChunkPartitionBounds.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RyserCoveringCounterexample.Selection.floor_chunkSize_posline 13 - theorem
OAI.RyserCoveringCounterexample.Selection.floor_chunkSize_leline 18 - theorem
OAI.RyserCoveringCounterexample.Selection.floor_chunkSize_ge_halfline 22 - theorem
OAI.RyserCoveringCounterexample.Selection.chunkCount_floor_leline 29 - theorem
OAI.RyserCoveringCounterexample.Selection.chunkCount_floor_le_natline 59