OAI/Combinatorics/RamseyFive/Marking/OrderedHighConflict.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.sum_symm_reindex line 12
2. def OAI.SharpRamseyFive.Marking.orderedHighCollision line 34
3. lemma OAI.SharpRamseyFive.Marking.orderedHighCollision_nonneg line 37
4. lemma OAI.SharpRamseyFive.Marking.orderedHighCollision_symm line 40
5. lemma OAI.SharpRamseyFive.Marking.orderedLaw_consistent line 44
6. lemma OAI.SharpRamseyFive.Marking.orderedHigh_collision_budget line 52
7. lemma OAI.SharpRamseyFive.Marking.orderedHigh_pair_impossible line 78
8. theorem OAI.SharpRamseyFive.Marking.high_three_domain_good_pair_impossible line 119
9. theorem OAI.SharpRamseyFive.Marking.high_three_domain_preRound_impossible line 150