OAI/Combinatorics/Ryser/Geometry/ProjectiveJoins.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.existsUnique_projectiveLine_of_ne line 9
  2. theorem OAI.RyserCoveringCounterexample.existsUnique_projectivePoint_of_ne line 51
  3. theorem OAI.RyserCoveringCounterexample.eq_projectiveLine_of_common_incidence line 89
  4. theorem OAI.RyserCoveringCounterexample.eq_projectivePoint_of_common_incidence line 97
  5. theorem OAI.RyserCoveringCounterexample.existsUnique_projective_incident_of_ne_lines line 105
  6. theorem OAI.RyserCoveringCounterexample.existsUnique_projectivePoint_of_ne_affineLines line 113
  7. theorem OAI.RyserCoveringCounterexample.eq_affineLine_of_common_projective_incidence line 119
  8. theorem OAI.RyserCoveringCounterexample.not_projectiveIncidence_infty_of_ne_direction line 128
  9. theorem OAI.RyserCoveringCounterexample.ne_of_projectiveIncidence_of_not_projectiveIncidence line 135