OAI/Combinatorics/Ryser/Incidence/PruningHigh.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RyserCoveringCounterexample.Incidence.high_degree_sum_leline 13 - theorem
OAI.RyserCoveringCounterexample.Incidence.incidenceCount_mono_leftline 33 - theorem
OAI.RyserCoveringCounterexample.Incidence.incidenceCount_mono_rightline 39 - theorem
OAI.RyserCoveringCounterexample.Incidence.high_degree_truncationline 45 - theorem
OAI.RyserCoveringCounterexample.Incidence.exists_pruned_coreline 82