OAI/Combinatorics/RamseyFive/Marking/MarkingEndpoints.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.Marking.mem_popularDomain line 21
2. lemma OAI.SharpRamseyFive.Marking.mem_poorDomain line 29
3. lemma OAI.SharpRamseyFive.Marking.typed_popular_second line 39
4. lemma OAI.SharpRamseyFive.Marking.typed_popular_partner line 63
5. lemma OAI.SharpRamseyFive.Marking.typed_poor_second line 95
6. lemma OAI.SharpRamseyFive.Marking.typed_poor_first line 111
7. def OAI.SharpRamseyFive.Marking.clampParameter line 140
8. lemma OAI.SharpRamseyFive.Marking.exp_clampParameter line 142
9. lemma OAI.SharpRamseyFive.Marking.clampParameter_bounds line 149
10. lemma OAI.SharpRamseyFive.Marking.clamped_reciprocal_caps line 154
11. lemma OAI.SharpRamseyFive.Marking.typedDomain_level_nonempty line 194
12. theorem OAI.SharpRamseyFive.Marking.typed_poor_reciprocal line 201