OAI/Combinatorics/Ryser/Incidence/WalkExpansion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Incidence.walkCard_mul_le_labelCard_pow_four line 17
2. theorem OAI.RyserCoveringCounterexample.Incidence.expansion_bound_of_card_mul_le line 40
3. theorem OAI.RyserCoveringCounterexample.Incidence.fourWalks_mem_data line 55
4. def OAI.RyserCoveringCounterexample.Incidence.edgeDifferences line 70
5. def OAI.RyserCoveringCounterexample.Incidence.differenceWalkLabels line 73
6. theorem OAI.RyserCoveringCounterexample.Incidence.differenceWalkLabels_injective line 77
7. theorem OAI.RyserCoveringCounterexample.Incidence.difference_bound_of_many_fourWalks line 96