OAI/Combinatorics/Ryser/Geometry/ProjectiveTransformAffine.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.translatePointMap line 9
  2. def OAI.RyserCoveringCounterexample.translateLineMap line 13
  3. theorem OAI.RyserCoveringCounterexample.translatePointMap_left_inv line 18
  4. theorem OAI.RyserCoveringCounterexample.translateLineMap_left_inv line 22
  5. def OAI.RyserCoveringCounterexample.translate line 33
  6. theorem OAI.RyserCoveringCounterexample.translate_points_finite line 75
  7. theorem OAI.RyserCoveringCounterexample.translate_points_infinite line 78
  8. theorem OAI.RyserCoveringCounterexample.translate_lines_infinity line 81
  9. theorem OAI.RyserCoveringCounterexample.translate_lines_vertical line 84
  10. theorem OAI.RyserCoveringCounterexample.translate_lines_slope line 87
  11. def OAI.RyserCoveringCounterexample.shearPointMap line 90
  12. def OAI.RyserCoveringCounterexample.shearLineMap line 95
  13. theorem OAI.RyserCoveringCounterexample.shearPointMap_left_inv line 100
  14. theorem OAI.RyserCoveringCounterexample.shearLineMap_left_inv line 107
  15. def OAI.RyserCoveringCounterexample.shear line 116
  16. theorem OAI.RyserCoveringCounterexample.shear_points_finite line 155
  17. theorem OAI.RyserCoveringCounterexample.shear_points_infinite_vertical line 158
  18. theorem OAI.RyserCoveringCounterexample.shear_points_infinite_slope line 161
  19. theorem OAI.RyserCoveringCounterexample.shear_lines_infinity line 164
  20. theorem OAI.RyserCoveringCounterexample.shear_lines_vertical line 167
  21. theorem OAI.RyserCoveringCounterexample.shear_lines_slope line 170
  22. def OAI.RyserCoveringCounterexample.scaleYPointMap line 173
  23. def OAI.RyserCoveringCounterexample.scaleYLineMap line 178
  24. theorem OAI.RyserCoveringCounterexample.scaleYPointMap_left_inv line 183
  25. theorem OAI.RyserCoveringCounterexample.scaleYLineMap_left_inv line 190
  26. def OAI.RyserCoveringCounterexample.scaleY line 199
  27. theorem OAI.RyserCoveringCounterexample.scaleY_points_finite line 240
  28. theorem OAI.RyserCoveringCounterexample.scaleY_points_infinite_vertical line 243
  29. theorem OAI.RyserCoveringCounterexample.scaleY_points_infinite_slope line 246
  30. theorem OAI.RyserCoveringCounterexample.scaleY_lines_infinity line 249
  31. theorem OAI.RyserCoveringCounterexample.scaleY_lines_vertical line 252
  32. theorem OAI.RyserCoveringCounterexample.scaleY_lines_slope line 255