OAI/Combinatorics/Ryser/Construction/DeletionParallel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Construction.deletedLines_inter_affinePencil_infinite_eq_filter line 16
2. theorem OAI.RyserCoveringCounterexample.Construction.card_deletedLines_inter_affinePencil_infinite line 26
3. theorem OAI.RyserCoveringCounterexample.Construction.allDeletedLines_inter_affinePencil_infinite_eq_biUnion line 35
4. theorem OAI.RyserCoveringCounterexample.Construction.card_allDeletedLines_inter_affinePencil_infinite_le line 57
5. theorem OAI.RyserCoveringCounterexample.Construction.card_groupDeletedLines_inter_affinePencil_infinite_le_two line 69