OAI/Combinatorics/RamseyFive/Marking/State.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.state line 13
2. lemma OAI.SharpRamseyFive.Marking.state_empty line 17
3. lemma OAI.SharpRamseyFive.Marking.state_insert line 24
4. lemma OAI.SharpRamseyFive.Marking.state_mono line 30
5. def OAI.SharpRamseyFive.Marking.Consistent line 37
6. lemma OAI.SharpRamseyFive.Marking.state_le_annihilator line 40
7. lemma OAI.SharpRamseyFive.Marking.state_rank_le line 49
8. lemma OAI.SharpRamseyFive.Marking.update_strict line 58
9. lemma OAI.SharpRamseyFive.Marking.subspace_finset_card line 74
10. def OAI.SharpRamseyFive.Marking.memberships line 80
11. lemma OAI.SharpRamseyFive.Marking.sum_memberships line 83
12. lemma OAI.SharpRamseyFive.Marking.q_mul_geometric_bound line 97
13. theorem OAI.SharpRamseyFive.Marking.popular_count line 105