OAI/Combinatorics/Ryser/LineCover/HighSamples.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RyserCoveringCounterexample.LineCover.PencilPopulation line 14
  2. abbrev OAI.RyserCoveringCounterexample.LineCover.ComplementPopulation line 17
  3. abbrev OAI.RyserCoveringCounterexample.LineCover.HighSample line 20
  4. theorem OAI.RyserCoveringCounterexample.LineCover.pencilPopulation_incident line 23
  5. theorem OAI.RyserCoveringCounterexample.LineCover.complementPopulation_mem line 27
  6. theorem OAI.RyserCoveringCounterexample.LineCover.complementPopulation_not_incident line 31
  7. theorem OAI.RyserCoveringCounterexample.LineCover.pencil_ne_complement line 38
  8. def OAI.RyserCoveringCounterexample.LineCover.highTuple line 45
  9. theorem OAI.RyserCoveringCounterexample.LineCover.highTuple_left line 60
  10. theorem OAI.RyserCoveringCounterexample.LineCover.highTuple_right line 64
  11. theorem OAI.RyserCoveringCounterexample.LineCover.highTuple_mem line 68
  12. def OAI.RyserCoveringCounterexample.LineCover.highCrossPairs line 74
  13. theorem OAI.RyserCoveringCounterexample.LineCover.mem_highCrossPairs line 79
  14. def OAI.RyserCoveringCounterexample.LineCover.highShapePairs line 85
  15. theorem OAI.RyserCoveringCounterexample.LineCover.mem_highShapePairs line 90
  16. def OAI.RyserCoveringCounterexample.LineCover.highSurvivorPairCount line 97