OAI/Combinatorics/Ryser/LineCover/Definitions.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RyserCoveringCounterexample.LineCover.LineTuple line 16
  2. def OAI.RyserCoveringCounterexample.LineCover.crossPoints line 18
  3. def OAI.RyserCoveringCounterexample.LineCover.FiniteCrossings line 22
  4. def OAI.RyserCoveringCounterexample.LineCover.tupleShapes line 25
  5. def OAI.RyserCoveringCounterexample.LineCover.AdmissibleTuple line 28
  6. def OAI.RyserCoveringCounterexample.LineCover.SparseShapes line 33
  7. def OAI.RyserCoveringCounterexample.LineCover.coverPencil line 37
  8. theorem OAI.RyserCoveringCounterexample.LineCover.mem_crossPoints line 41
  9. theorem OAI.RyserCoveringCounterexample.LineCover.mem_tupleShapes line 46
  10. theorem OAI.RyserCoveringCounterexample.LineCover.mem_coverPencil line 51
  11. theorem OAI.RyserCoveringCounterexample.LineCover.coverPencil_subset line 56
  12. theorem OAI.RyserCoveringCounterexample.LineCover.left_ne_right line 59