OAI/Combinatorics/RamseyFive/Marking/HighLowConflict.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.highThreeLeft line 19
2. def OAI.SharpRamseyFive.Marking.highThreeRight line 21
3. def OAI.SharpRamseyFive.Marking.highThreeGood line 23
4. def OAI.SharpRamseyFive.Marking.highCollision line 27
5. lemma OAI.SharpRamseyFive.Marking.high_collision_nonneg line 31
6. lemma OAI.SharpRamseyFive.Marking.high_three_core_slack line 34
7. theorem OAI.SharpRamseyFive.Marking.high_three_collisions line 41
8. lemma OAI.SharpRamseyFive.Marking.high_three_low_conflict line 69
9. theorem OAI.SharpRamseyFive.Marking.high_three_pair_impossible line 79
10. theorem OAI.SharpRamseyFive.Marking.marking_high_endpoint_bad line 118
11. lemma OAI.SharpRamseyFive.Marking.marking_high_three_mass line 145