OAI/Combinatorics/SharpRamsey/Geometry/PreparedRadial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.GreedyPreparation.list_union_inter_card_le line 15
2. theorem OAI.SharpLogRamsey.GreedyPreparation.prepared_list_radial line 28
3. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.planePoints line 126
4. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.mem_planePoints line 129
5. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.points_mono line 132
6. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.join_eq_line line 138
7. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.line_inter_points_le_one line 144
8. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.distinct_lines_inter_le_one line 157
9. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.ProjectiveLine line 168
10. instance OAI.SharpLogRamsey.PreparedProjectiveGeometry.flat_JoinedPreparedRadial_5 line 169
11. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.projective_prepared_radial line 171