OAI/Combinatorics/RamseyFive/Geometry/FlatPoints.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ProjectiveTraining.flatPoints line 16
  2. lemma OAI.SharpRamseyFive.ProjectiveTraining.mem_flatPoints line 21
  3. lemma OAI.SharpRamseyFive.ProjectiveTraining.inter_flatPoints line 25
  4. lemma OAI.SharpRamseyFive.ProjectiveTraining.line_covered_cap line 30
  5. lemma OAI.SharpRamseyFive.ProjectiveTraining.plane_covered_cap line 45
  6. lemma OAI.SharpRamseyFive.ProjectiveTraining.captured_cover line 63
  7. lemma OAI.SharpRamseyFive.ProjectiveTraining.rich_line_has_containing_flat line 75
  8. lemma OAI.SharpRamseyFive.ProjectiveTraining.head_plane_points line 90
  9. lemma OAI.SharpRamseyFive.ProjectiveTraining.atlas_head_tail_cap line 104
  10. lemma OAI.SharpRamseyFive.ProjectiveTraining.outside_cell_earlier line 111
  11. lemma OAI.SharpRamseyFive.ProjectiveTraining.earliest_line_outside_cell_cap line 120
  12. lemma OAI.SharpRamseyFive.ProjectiveTraining.earliest_plane_outside_cell_cap line 141
  13. lemma OAI.SharpRamseyFive.ProjectiveTraining.surviving_line_center_earlier line 162
  14. lemma OAI.SharpRamseyFive.ProjectiveTraining.surviving_plane_center_earlier line 178
  15. lemma OAI.SharpRamseyFive.ProjectiveTraining.surviving_line_centers_cap line 195
  16. lemma OAI.SharpRamseyFive.ProjectiveTraining.surviving_plane_centers_cap line 217
  17. def OAI.SharpRamseyFive.ProjectiveTraining.cellRichLines line 239
  18. lemma OAI.SharpRamseyFive.ProjectiveTraining.cell_filter_own_flat line 244
  19. lemma OAI.SharpRamseyFive.ProjectiveTraining.card_cellRichLines_le line 252
  20. lemma OAI.SharpRamseyFive.ProjectiveTraining.cellRichLines_variance line 260
  21. theorem OAI.SharpRamseyFive.ProjectiveTraining.weighted_cell_rich_lines line 285
  22. def OAI.SharpRamseyFive.ProjectiveTraining.capturedLineCenters line 334
  23. lemma OAI.SharpRamseyFive.ProjectiveTraining.earliest_line_cell_rich line 340
  24. theorem OAI.SharpRamseyFive.ProjectiveTraining.captured_center_line_count line 356