OAI/Combinatorics/RamseyFive/Marking/ScanChoice.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.scanChoice line 16
2. lemma OAI.SharpRamseyFive.Marking.scanChoice_isSome line 23
3. theorem OAI.SharpRamseyFive.Marking.scanSet_card_bound line 33
4. def OAI.SharpRamseyFive.Marking.popularDomain line 99
5. def OAI.SharpRamseyFive.Marking.poorDomain line 105
6. theorem OAI.SharpRamseyFive.Marking.popularDomain_card line 111
7. theorem OAI.SharpRamseyFive.Marking.poorDomain_card line 117
8. lemma OAI.SharpRamseyFive.Marking.scan_annihilator line 125
9. theorem OAI.SharpRamseyFive.Marking.cheap_mem_domains line 138
10. lemma OAI.SharpRamseyFive.Marking.state_congr_on line 170