OAI/Combinatorics/Ryser/Construction/GadgetDefinitions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RyserCoveringCounterexample.Construction.NonzeroSlope line 11
2. abbrev OAI.RyserCoveringCounterexample.Construction.GadgetOutcome line 13
3. def OAI.RyserCoveringCounterexample.Construction.omittedLine line 15
4. def OAI.RyserCoveringCounterexample.Construction.retainedPoints line 18
5. def OAI.RyserCoveringCounterexample.Construction.transformedRetained line 21
6. def OAI.RyserCoveringCounterexample.Construction.cubicDeletionUnion line 24
7. theorem OAI.RyserCoveringCounterexample.Construction.mem_retainedPoints line 27
8. theorem OAI.RyserCoveringCounterexample.Construction.not_incidence_omittedLine line 31
9. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_mem_cubicShape_iff line 35
10. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_mem_transformedRetained_iff line 49
11. theorem OAI.RyserCoveringCounterexample.Construction.transformedRetained_eq_survivors line 60
12. theorem OAI.RyserCoveringCounterexample.Construction.transformedRetained_card line 69
13. theorem OAI.RyserCoveringCounterexample.Construction.omitted_line_disjoint_retained line 74