OAI/Combinatorics/SharpRamsey/Geometry/PencilGeometry.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.RadialLine line 19
  2. instance OAI.SharpLogRamsey.PreparedProjectiveGeometry.radialLineFintype line 22
  3. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.lines line 26
  4. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.mem_lines line 30
  5. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.finrank_join line 35
  6. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.radial_unique line 46
  7. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.radialFiber line 51
  8. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.mem_radialFiber line 56
  9. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.radialFiber_disjoint line 62
  10. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.radial_biUnion line 71
  11. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.radial_count line 85
  12. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.radial_mass line 93
  13. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.hyperplane_mass line 99
  14. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.intersection_mass line 105
  15. lemma OAI.SharpLogRamsey.CertificateGeometry.through_iff line 131
  16. theorem OAI.SharpLogRamsey.CertificateGeometry.card_through line 137
  17. theorem OAI.SharpLogRamsey.CertificateGeometry.line_card line 145
  18. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.point_dualCoannihilator line 173
  19. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.intersection_finrank line 181
  20. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.strength line 191
  21. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.overlap line 194
  22. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.overlap_is_strength line 198
  23. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.hyperplanes_on_line_card_le line 208
  24. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.richRadials line 223
  25. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.hyperplanesOn line 226
  26. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.largePairs line 230
  27. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.largePairs_card line 234
  28. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.largeNeighbors line 260
  29. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.neighbors_card line 265
  30. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.largeNeighbors_bound line 286
  31. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.overlap_plane_zero line 318
  32. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.one_direction_card line 355
  33. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.two_directions_card line 376
  34. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.pencil_card line 401