OAI/Combinatorics/Ryser/Geometry/ProjectiveTransformXZ.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.swapXZPoint line 9
  2. def OAI.RyserCoveringCounterexample.swapXZLine line 17
  3. theorem OAI.RyserCoveringCounterexample.swapXZPoint_finite_zero line 24
  4. theorem OAI.RyserCoveringCounterexample.swapXZPoint_finite_of_ne_zero line 29
  5. theorem OAI.RyserCoveringCounterexample.swapXZPoint_infinite_slope line 34
  6. theorem OAI.RyserCoveringCounterexample.swapXZPoint_infinite_vertical line 37
  7. theorem OAI.RyserCoveringCounterexample.swapXZLine_infinity line 40
  8. theorem OAI.RyserCoveringCounterexample.swapXZLine_vertical_zero line 43
  9. theorem OAI.RyserCoveringCounterexample.swapXZLine_vertical_of_ne_zero line 48
  10. theorem OAI.RyserCoveringCounterexample.swapXZLine_sloped line 53
  11. theorem OAI.RyserCoveringCounterexample.swapXZPoint_involutive line 56
  12. theorem OAI.RyserCoveringCounterexample.swapXZLine_involutive line 71
  13. theorem OAI.RyserCoveringCounterexample.swapXZ_incidence line 86
  14. def OAI.RyserCoveringCounterexample.swapXZ line 149
  15. theorem OAI.RyserCoveringCounterexample.swapXZ_points line 162
  16. theorem OAI.RyserCoveringCounterexample.swapXZ_lines line 165
  17. theorem OAI.RyserCoveringCounterexample.swapXZ_points_finite_zero line 168
  18. theorem OAI.RyserCoveringCounterexample.swapXZ_points_finite_of_ne_zero line 172
  19. theorem OAI.RyserCoveringCounterexample.swapXZ_points_infinite_slope line 176
  20. theorem OAI.RyserCoveringCounterexample.swapXZ_points_infinite_vertical line 179
  21. theorem OAI.RyserCoveringCounterexample.swapXZ_lines_infinity line 182
  22. theorem OAI.RyserCoveringCounterexample.swapXZ_lines_vertical_zero line 185
  23. theorem OAI.RyserCoveringCounterexample.swapXZ_lines_vertical_of_ne_zero line 189
  24. theorem OAI.RyserCoveringCounterexample.swapXZ_lines_sloped line 193