OAI/Combinatorics/RamseyFive/Marking/ChooseLevel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.Marking.card_upper line 15
2. lemma OAI.SharpRamseyFive.Marking.exists_level line 21
3. def OAI.SharpRamseyFive.Marking.chooseLevel line 34
4. lemma OAI.SharpRamseyFive.Marking.chooseLevel_le line 37
5. lemma OAI.SharpRamseyFive.Marking.chooseLevel_large line 40
6. lemma OAI.SharpRamseyFive.Marking.chooseLevel_nonempty line 44
7. lemma OAI.SharpRamseyFive.Marking.chooseLevel_sublevel line 56
8. lemma OAI.SharpRamseyFive.Marking.coannihilator_card_bound line 73
9. theorem OAI.SharpRamseyFive.Marking.popular_joint_count line 93
10. def OAI.SharpRamseyFive.Marking.Expensive line 134
11. def OAI.SharpRamseyFive.Marking.scanSet line 140
12. def OAI.SharpRamseyFive.Marking.scanState line 145
13. lemma OAI.SharpRamseyFive.Marking.scanSet_subset line 149
14. lemma OAI.SharpRamseyFive.Marking.scanSet_mono line 163
15. lemma OAI.SharpRamseyFive.Marking.scanState_mono line 171
16. lemma OAI.SharpRamseyFive.Marking.scanState_update line 177
17. lemma OAI.SharpRamseyFive.Marking.scan_rank line 189
18. lemma OAI.SharpRamseyFive.Marking.scan_count line 206