OAI/Combinatorics/SharpRamsey/Marking/MarkingTwoScans.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.Marking.pairDuality line 17
2. def OAI.SharpLogRamsey.Marking.reversedPairs line 24
3. lemma OAI.SharpLogRamsey.Marking.reversedPairs_consistent line 29
4. lemma OAI.SharpLogRamsey.Marking.reversedPairs_incident line 43
5. abbrev OAI.SharpLogRamsey.Marking.TwoMask line 48
6. def OAI.SharpLogRamsey.Marking.twoMask line 51
7. def OAI.SharpLogRamsey.Marking.bothExpensive line 54
8. lemma OAI.SharpLogRamsey.Marking.bothExpensive_mem line 60
9. abbrev OAI.SharpLogRamsey.Marking.TwoMessage line 72
10. def OAI.SharpLogRamsey.Marking.firstMessage line 75
11. def OAI.SharpLogRamsey.Marking.secondMessage line 80
12. def OAI.SharpLogRamsey.Marking.cheapBoth line 85
13. lemma OAI.SharpLogRamsey.Marking.firstMessage_actual line 90
14. lemma OAI.SharpLogRamsey.Marking.secondMessage_actual line 106
15. lemma OAI.SharpLogRamsey.Marking.cheapBoth_mem line 125
16. lemma OAI.SharpLogRamsey.Marking.cheapBoth_card line 147
17. lemma OAI.SharpLogRamsey.Marking.cheapBoth_log_card line 154
18. lemma OAI.SharpLogRamsey.Marking.bothExpensive_card line 165