OAI/Combinatorics/Ryser/Construction/ExtraDirections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.directionMap_bijective line 12
2. theorem OAI.RyserCoveringCounterexample.Construction.extra_placedDirection line 18
3. theorem OAI.RyserCoveringCounterexample.Construction.extra_allDirections_image line 43
4. theorem OAI.RyserCoveringCounterexample.Construction.extra_axisDirections line 60
5. theorem OAI.RyserCoveringCounterexample.Construction.alteredDirections_eq_allDirections_sdiff_axisDirections line 65
6. theorem OAI.RyserCoveringCounterexample.Construction.extra_alteredDirections line 84
7. theorem OAI.RyserCoveringCounterexample.Construction.none_mem_extra_alteredDirections line 90
8. theorem OAI.RyserCoveringCounterexample.Construction.zero_mem_extra_alteredDirections line 98
9. theorem OAI.RyserCoveringCounterexample.Construction.diagonal_one_axisDirections_subset_extra_alteredDirections line 117
10. theorem OAI.RyserCoveringCounterexample.Construction.extra_axisDirections_subset_diagonal_one_alteredDirections line 131