OAI/Combinatorics/Ryser/LineCover/LowDegeneracy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.natCard_le_mul_of_fibers line 17
  2. def OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.SameDirection line 34
  3. def OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.Concurrent line 37
  4. def OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.firstPair line 40
  5. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.firstPair_zero line 43
  6. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.firstPair_one line 46
  7. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.pair_lines_ne line 49
  8. def OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.pairMeet line 55
  9. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.pairMeet_incident line 58
  10. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.eq_pairMeet line 64
  11. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.card_sameDirection_le line 71
  12. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.card_concurrent_le line 98
  13. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_le_of_card line 139
  14. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_sameDirection_le line 164
  15. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_concurrent_le line 176
  16. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_exists_restrict_le line 188
  17. def OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.AnyParallel line 208
  18. def OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.AnyConcurrent line 211
  19. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.anyParallel_iff line 214
  20. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.anyConcurrent_iff line 228
  21. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_anyParallel_le line 254
  22. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_anyConcurrent_le line 269
  23. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_tuple_parallel_le line 285
  24. theorem OAI.RyserCoveringCounterexample.LineCover.LowDegeneracy.prob_tuple_concurrent_le line 295