OAI/Combinatorics/Ryser/Construction/GadgetGood.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RyserCoveringCounterexample.Construction.GoodGadget line 13
2. theorem OAI.RyserCoveringCounterexample.Construction.gadgetConfig_survivors_ignoring_line line 19
3. theorem OAI.RyserCoveringCounterexample.Construction.gadget_line_density_of_goodLineCover line 31
4. theorem OAI.RyserCoveringCounterexample.Construction.gadget_near_pencil_of_goodLineCover line 43
5. theorem OAI.RyserCoveringCounterexample.Construction.goodGadget_of_events line 69
6. theorem OAI.RyserCoveringCounterexample.Construction.GoodGadget.retained_nonempty line 80