OAI/Combinatorics/Ryser/LineCover/Overlap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.LineCover.multiplicity line 16
  2. def OAI.RyserCoveringCounterexample.LineCover.coveredPoints line 19
  3. def OAI.RyserCoveringCounterexample.LineCover.overlapExcess line 22
  4. def OAI.RyserCoveringCounterexample.LineCover.orderedPairMass line 25
  5. def OAI.RyserCoveringCounterexample.LineCover.heavyPoints line 28
  6. theorem OAI.RyserCoveringCounterexample.LineCover.incidence_double_count line 31
  7. theorem OAI.RyserCoveringCounterexample.LineCover.sum_multiplicity_eq_covered_add_excess line 37
  8. theorem OAI.RyserCoveringCounterexample.LineCover.incidence_eq_covered_add_excess line 53
  9. theorem OAI.RyserCoveringCounterexample.LineCover.covered_add_uncovered_card line 59
  10. theorem OAI.RyserCoveringCounterexample.LineCover.cover_count_bounds line 65
  11. theorem OAI.RyserCoveringCounterexample.LineCover.heavyPoints_card_mul_le_excess line 110
  12. theorem OAI.RyserCoveringCounterexample.LineCover.orderedPairMass_le_light_add_heavy line 130