OAI/Combinatorics/Ryser/Incidence/PruningCore.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Incidence.leftDegree line 17
  2. def OAI.RyserCoveringCounterexample.Incidence.rightDegree line 21
  3. def OAI.RyserCoveringCounterexample.Incidence.incidenceCount line 24
  4. theorem OAI.RyserCoveringCounterexample.Incidence.leftDegree_eq_sum line 27
  5. theorem OAI.RyserCoveringCounterexample.Incidence.incidenceCount_swap line 32
  6. theorem OAI.RyserCoveringCounterexample.Incidence.leftDegree_mono line 38
  7. theorem OAI.RyserCoveringCounterexample.Incidence.rightDegree_mono line 43
  8. theorem OAI.RyserCoveringCounterexample.Incidence.incidenceCount_erase_left line 47
  9. theorem OAI.RyserCoveringCounterexample.Incidence.incidenceCount_erase_right line 52
  10. def OAI.RyserCoveringCounterexample.Incidence.pruningPotential line 58
  11. theorem OAI.RyserCoveringCounterexample.Incidence.pruningPotential_le_erase_left line 61
  12. theorem OAI.RyserCoveringCounterexample.Incidence.pruningPotential_le_erase_right line 74
  13. def OAI.RyserCoveringCounterexample.Incidence.MinimumDegrees line 87
  14. theorem OAI.RyserCoveringCounterexample.Incidence.exists_degree_core_aux line 91
  15. theorem OAI.RyserCoveringCounterexample.Incidence.exists_degree_core line 131
  16. theorem OAI.RyserCoveringCounterexample.Incidence.degree_core_incidence_lower_bound line 136