OAI/Combinatorics/Ryser/Geometry/ProjectiveTransformXY.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.swapXYDirection line 10
  2. theorem OAI.RyserCoveringCounterexample.swapXYDirection_none line 16
  3. theorem OAI.RyserCoveringCounterexample.swapXYDirection_zero line 19
  4. theorem OAI.RyserCoveringCounterexample.swapXYDirection_nonzero line 22
  5. theorem OAI.RyserCoveringCounterexample.swapXYDirection_involutive line 25
  6. def OAI.RyserCoveringCounterexample.swapXYPoint line 36
  7. theorem OAI.RyserCoveringCounterexample.swapXYPoint_involutive line 40
  8. def OAI.RyserCoveringCounterexample.swapXYAffineLine line 49
  9. theorem OAI.RyserCoveringCounterexample.swapXYAffineLine_direction line 55
  10. theorem OAI.RyserCoveringCounterexample.swapXYAffineLine_involutive line 64
  11. def OAI.RyserCoveringCounterexample.swapXYLine line 75
  12. theorem OAI.RyserCoveringCounterexample.swapXYLine_involutive line 79
  13. theorem OAI.RyserCoveringCounterexample.swapXY_projection_equation line 88
  14. theorem OAI.RyserCoveringCounterexample.swapXY_affine_incidence line 95
  15. theorem OAI.RyserCoveringCounterexample.swapXY_incidence line 108
  16. def OAI.RyserCoveringCounterexample.swapXY line 124
  17. theorem OAI.RyserCoveringCounterexample.swapXY_points_finite line 137
  18. theorem OAI.RyserCoveringCounterexample.swapXY_points_infinite line 140
  19. theorem OAI.RyserCoveringCounterexample.swapXY_lines_infinity line 143
  20. theorem OAI.RyserCoveringCounterexample.swapXY_lines_affine line 146
  21. theorem OAI.RyserCoveringCounterexample.swapXY_lines_vertical line 149
  22. theorem OAI.RyserCoveringCounterexample.swapXY_lines_slope_zero line 152
  23. theorem OAI.RyserCoveringCounterexample.swapXY_lines_slope_nonzero line 157