OAI/Combinatorics/RamseyFive/Geometry/PlaneCommonNeighbors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.RichPlaneOverlap.plane_common_neighbors line 16
2. theorem OAI.SharpRamseyFive.RichPlaneOverlap.inf_eq_point_of_not_line line 38
3. theorem OAI.SharpRamseyFive.RichPlaneOverlap.local_skew_pairs line 53
4. theorem OAI.SharpRamseyFive.RichPlaneOverlap.sum_point_pairs_le line 97
5. theorem OAI.SharpRamseyFive.RichPlaneOverlap.high_degree_second_moment line 116
6. theorem OAI.SharpRamseyFive.RichPlaneOverlap.plane_point_double_count line 133
7. theorem OAI.SharpRamseyFive.RichPlaneOverlap.rich_plane_count line 139