OAI/Combinatorics/SharpRamsey/Geometry/SpanPairLine.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for rich lines and finite point configurations.

  1. lemma OAI.SharpLogRamsey.ProjectiveLineChart.span_pair_of_line line 18
  2. lemma OAI.SharpLogRamsey.ProjectiveLineChart.normalized_span line 39
  3. theorem OAI.SharpLogRamsey.ProjectiveLineChart.coord_mem_line line 51
  4. lemma OAI.SharpLogRamsey.ProjectiveLineChart.line_coord_ne line 60
  5. theorem OAI.SharpLogRamsey.ProjectiveLineChart.carriers_injective line 68
  6. theorem OAI.SharpLogRamsey.RichProjectiveLines.card_lines_square line 111
  7. theorem OAI.SharpLogRamsey.RichProjectiveLines.card_mul_le line 136
  8. theorem OAI.SharpLogRamsey.RichLineScales.choose_parameters line 204
  9. theorem OAI.SharpLogRamsey.RichProjectiveCount.card_mul_le line 286
  10. theorem OAI.SharpLogRamsey.RichFiniteProjective.card_mul_le line 320