OAI/Combinatorics/Ryser/Construction/ExceptionalCover.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.ActiveExceptional line 13
  2. def OAI.RyserCoveringCounterexample.Construction.LineCapable line 17
  3. def OAI.RyserCoveringCounterexample.Construction.lineResources line 23
  4. def OAI.RyserCoveringCounterexample.Construction.pointResources line 30
  5. theorem OAI.RyserCoveringCounterexample.Construction.mem_lineResources line 37
  6. theorem OAI.RyserCoveringCounterexample.Construction.mem_pointResources line 46
  7. theorem OAI.RyserCoveringCounterexample.Construction.lineResources_subset line 55
  8. theorem OAI.RyserCoveringCounterexample.Construction.pointResources_subset line 62
  9. theorem OAI.RyserCoveringCounterexample.Construction.lineResources_disjoint_pointResources line 69
  10. theorem OAI.RyserCoveringCounterexample.Construction.lineResources_disjoint_other_of_axis_subset line 78
  11. theorem OAI.RyserCoveringCounterexample.Construction.forcedPencilVertices_no_action_of_altered line 102
  12. theorem OAI.RyserCoveringCounterexample.Construction.exceptional_cover_of_vertex_cover line 120
  13. theorem OAI.RyserCoveringCounterexample.Construction.exceptional_cover_sdiff_of_no_action line 127
  14. theorem OAI.RyserCoveringCounterexample.Construction.exceptional_cover_additional_of_altered line 138
  15. theorem OAI.RyserCoveringCounterexample.Construction.lineCapable_has_line line 159
  16. theorem OAI.RyserCoveringCounterexample.Construction.not_lineCapable_unique line 193
  17. theorem OAI.RyserCoveringCounterexample.Construction.not_lineCapable_has_point line 214
  18. theorem OAI.RyserCoveringCounterexample.Construction.exceptional_resource_has_line line 227
  19. theorem OAI.RyserCoveringCounterexample.Construction.exists_line_cover_of_exceptional_cover line 241
  20. theorem OAI.RyserCoveringCounterexample.Construction.exists_mixed_cover_of_exceptional_cover line 257