OAI/Combinatorics/RamseyFive/Marking/ReciprocalBands.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.Marking.BandCondition line 15
2. lemma OAI.SharpRamseyFive.Marking.exists_reciprocal_band line 19
3. lemma OAI.SharpRamseyFive.Marking.popular_reciprocal_caps line 49
4. lemma OAI.SharpRamseyFive.Marking.high_rank_cases line 70
5. lemma OAI.SharpRamseyFive.Marking.zero_level_memberships line 83
6. lemma OAI.SharpRamseyFive.Marking.typed_popular_rank_pos line 97
7. lemma OAI.SharpRamseyFive.Marking.closed_band_slack line 119
8. lemma OAI.SharpRamseyFive.Marking.open_band_slack line 133
9. theorem OAI.SharpRamseyFive.Marking.closed_reciprocal_ranks line 150
10. theorem OAI.SharpRamseyFive.Marking.open_reciprocal_ranks line 162