OAI/Combinatorics/Ryser/Construction/GadgetOriginalCounts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RyserCoveringCounterexample.Construction.originalLineSurvivors line 15
2. def OAI.RyserCoveringCounterexample.Construction.originalLineCount line 20
3. theorem OAI.RyserCoveringCounterexample.Construction.mem_originalLineSurvivors line 23
4. theorem OAI.RyserCoveringCounterexample.Construction.originalLineSurvivors_eq_retained_filter line 30
5. theorem OAI.RyserCoveringCounterexample.Construction.originalLineCount_eq_retained_filter_card line 50
6. theorem OAI.RyserCoveringCounterexample.Construction.originalLineSurvivors_update_same line 56
7. theorem OAI.RyserCoveringCounterexample.Construction.originalLineSurvivors_card_le_add_one_of_agree_off line 71
8. theorem OAI.RyserCoveringCounterexample.Construction.originalLineCount_update_abs_le line 120