OAI/Combinatorics/Ryser/Geometry/AffineJoins.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.point_eq_of_projection_eq_of_ne_direction line 10
  2. theorem OAI.RyserCoveringCounterexample.line_eq_of_direction_eq_of_incidence line 54
  3. theorem OAI.RyserCoveringCounterexample.not_incidence_of_same_direction_of_ne line 62
  4. theorem OAI.RyserCoveringCounterexample.line_eq_of_two_incident_points line 67
  5. theorem OAI.RyserCoveringCounterexample.eq_of_common_incidence_of_ne_lines line 80
  6. theorem OAI.RyserCoveringCounterexample.existsUnique_incident_of_ne_direction line 87
  7. def OAI.RyserCoveringCounterexample.joinDirection line 135
  8. def OAI.RyserCoveringCounterexample.joinLine line 138
  9. theorem OAI.RyserCoveringCounterexample.incidence_joinLine_left line 141
  10. theorem OAI.RyserCoveringCounterexample.incidence_joinLine_right line 144
  11. theorem OAI.RyserCoveringCounterexample.lineThrough_joinDirection_eq line 166
  12. theorem OAI.RyserCoveringCounterexample.eq_joinLine_of_incidence line 173
  13. theorem OAI.RyserCoveringCounterexample.existsUnique_lineThrough_pair line 179
  14. theorem OAI.RyserCoveringCounterexample.projection_eq_iff_eq_joinDirection line 186
  15. theorem OAI.RyserCoveringCounterexample.existsUnique_direction_of_ne line 205