OAI/Combinatorics/Ryser/LineCover/CleanCover.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RyserCoveringCounterexample.LineCover.cleanLines line 14
2. theorem OAI.RyserCoveringCounterexample.LineCover.cleanLines_subset line 17
3. theorem OAI.RyserCoveringCounterexample.LineCover.cleanLines_not_selected line 20
4. theorem OAI.RyserCoveringCounterexample.LineCover.survivor_incidence_not_selected line 24
5. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_inter_cleanLines line 31
6. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_sdiff_cleanLines line 49
7. theorem OAI.RyserCoveringCounterexample.LineCover.coverPencil_mono line 69
8. theorem OAI.RyserCoveringCounterexample.LineCover.coveredPoints_eq_inter_biUnion line 75
9. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_ignore_tuple_eq line 96