OAI/Combinatorics/Ryser/Construction/FiniteSelectionCounting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Construction.exists_selection_card_eq line 11
2. theorem OAI.RyserCoveringCounterexample.Construction.exists_five_selection line 29
3. def OAI.RyserCoveringCounterexample.Construction.selectedPositions line 39
4. theorem OAI.RyserCoveringCounterexample.Construction.mem_selectedPositions line 42
5. theorem OAI.RyserCoveringCounterexample.Construction.card_selectedPositions_eq_sum line 48
6. theorem OAI.RyserCoveringCounterexample.Construction.card_selectedPositions line 68
7. theorem OAI.RyserCoveringCounterexample.Construction.card_eq_card_image_fst_of_one_per_group line 77
8. theorem OAI.RyserCoveringCounterexample.Construction.card_le_card_image_fst_of_one_per_group line 90
9. theorem OAI.RyserCoveringCounterexample.Construction.card_le_selected_group_of_subset line 96
10. theorem OAI.RyserCoveringCounterexample.Construction.card_le_five_of_subset_selectedPositions_one_group line 110