OAI/Combinatorics/RamseyFive/Marking/MarkingClassDomains.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.reversedMarkingDomain line 17
2. lemma OAI.SharpRamseyFive.Marking.markingDomain_forward line 21
3. lemma OAI.SharpRamseyFive.Marking.markingDomain_backward line 25
4. lemma OAI.SharpRamseyFive.Marking.endpoint_card_mono line 34
5. lemma OAI.SharpRamseyFive.Marking.reversedDomain_first_card line 41
6. lemma OAI.SharpRamseyFive.Marking.reversedDomain_second_card line 49
7. def OAI.SharpRamseyFive.Marking.ForwardCaps line 58
8. def OAI.SharpRamseyFive.Marking.ReverseCaps line 62
9. lemma OAI.SharpRamseyFive.Marking.marking_poor_forward line 66
10. lemma OAI.SharpRamseyFive.Marking.marking_poor_backward line 82
11. lemma OAI.SharpRamseyFive.Marking.marking_popular_caps line 100
12. lemma OAI.SharpRamseyFive.Marking.marking_popular_partners_first line 123
13. lemma OAI.SharpRamseyFive.Marking.marking_popular_partners_second line 146
14. theorem OAI.SharpRamseyFive.Marking.marking_domain_dichotomy line 167