OAI/Combinatorics/Ryser/Incidence/AllLineCap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Incidence.leftDegree_le_erase_add_one line 14
2. theorem OAI.RyserCoveringCounterexample.Incidence.rightDegree_mul_sub_one_le line 26
3. theorem OAI.RyserCoveringCounterexample.Incidence.rightDegree_le_div_sub_one line 67
4. theorem OAI.RyserCoveringCounterexample.Incidence.projective_all_line_cap line 77