OAI/Combinatorics/RamseyFive/Bounds/UpperSet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.upperSet line 12
2. def OAI.SharpRamseyFive.Marking.levelSet line 15
3. def OAI.SharpRamseyFive.Marking.nextState line 18
4. lemma OAI.SharpRamseyFive.Marking.nextState_mono line 23
5. lemma OAI.SharpRamseyFive.Marking.nextState_upper_subset line 30
6. lemma OAI.SharpRamseyFive.Marking.leaves_upper line 37
7. theorem OAI.SharpRamseyFive.Marking.expensive_contraction line 50