OAI/Combinatorics/BalancedRyser/Incidence/PencilOccupancy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.card_le_exceptional_add_cover_budget line 13
2. theorem OAI.Balanced.pencil_cover_card_bound line 32
3. theorem OAI.Balanced.affine_pencil_cover_card_bound line 46
4. theorem OAI.Balanced.parallel_pencil_cover_card_bound line 55