OAI/Combinatorics/SharpRamsey/Marking/MarkingTwoCaps.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.Marking.twoDomain line 16
2. lemma OAI.SharpLogRamsey.Marking.twoDomain_forward line 22
3. lemma OAI.SharpLogRamsey.Marking.twoDomain_reverse line 27
4. lemma OAI.SharpLogRamsey.Marking.shadow_reverse_first line 39
5. lemma OAI.SharpLogRamsey.Marking.shadow_reverse_second_card line 53
6. theorem OAI.SharpLogRamsey.Marking.twoPopular_caps line 68
7. theorem OAI.SharpLogRamsey.Marking.twoPoor_product line 107
8. lemma OAI.SharpLogRamsey.Marking.nonempty_cheap_not_expensive line 135
9. theorem OAI.SharpLogRamsey.Marking.twoDomain_cases line 144