OAI/Combinatorics/RamseyFive/Decoding/PairPoints.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ActualOverlap.pairPoints line 13
2. theorem OAI.SharpRamseyFive.ActualOverlap.nondominant_pair_count line 16
3. theorem OAI.SharpRamseyFive.ActualOverlap.nondominant_degree_count line 54
4. def OAI.SharpRamseyFive.ActualOverlap.richRadials line 98
5. theorem OAI.SharpRamseyFive.ActualOverlap.dominant_degree_count line 102
6. theorem OAI.SharpRamseyFive.ActualOverlap.dominant_pair_count line 134
7. theorem OAI.SharpRamseyFive.ActualOverlap.intersection_radial_three line 159
8. theorem OAI.SharpRamseyFive.ActualOverlap.overlap_dichotomy line 171
9. theorem OAI.SharpRamseyFive.ActualOverlap.pair_count_three line 204
10. theorem OAI.SharpRamseyFive.ActualOverlap.degree_count_three line 220
11. def OAI.SharpRamseyFive.ActualOverlap.overlapPairs line 236
12. def OAI.SharpRamseyFive.ActualOverlap.overlapNeighbors line 240
13. theorem OAI.SharpRamseyFive.ActualOverlap.actual_pair_count_four line 244
14. theorem OAI.SharpRamseyFive.ActualOverlap.actual_degree_count_four line 280