OAI/Combinatorics/RamseyFive/Geometry/ExceptionalCenters.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpRamseyFive.RichPlaneOverlap.exceptional_centers line 13
  2. lemma OAI.SharpRamseyFive.RichPlaneGeometry.inf_eq_shared_line line 44
  3. theorem OAI.SharpRamseyFive.RichPlaneGeometry.rich_planes_through_line line 58
  4. theorem OAI.SharpRamseyFive.RichPlaneGeometry.rich_planes_through_line_twice line 113
  5. def OAI.SharpRamseyFive.RichPlaneGeometry.dualOfHyperplane line 124
  6. lemma OAI.SharpRamseyFive.RichPlaneGeometry.ker_dualOfHyperplane line 131
  7. lemma OAI.SharpRamseyFive.RichPlaneGeometry.dualOfHyperplane_injective line 145