OAI/Combinatorics/Ryser/Construction/DeletionUnionBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RyserCoveringCounterexample.Construction.DeletionSeparated line 13
2. def OAI.RyserCoveringCounterexample.Construction.allDeletedLines line 19
3. def OAI.RyserCoveringCounterexample.Construction.deletedPencil line 23
4. def OAI.RyserCoveringCounterexample.Construction.activeDeletionGroups line 27
5. theorem OAI.RyserCoveringCounterexample.Construction.mem_allDeletedLines line 31
6. theorem OAI.RyserCoveringCounterexample.Construction.mem_deletedPencil line 36
7. theorem OAI.RyserCoveringCounterexample.Construction.mem_activeDeletionGroups line 42
8. theorem OAI.RyserCoveringCounterexample.Construction.not_incidence_deletedLines_of_mem_other_subplane line 48
9. theorem OAI.RyserCoveringCounterexample.Construction.disjoint_deletedLines_of_separated line 62