OAI/Combinatorics/Ryser/Geometry/Normalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.exists_direction_of_incidence_infinity line 11
2. theorem OAI.RyserCoveringCounterexample.exists_affine_of_not_incidence_infinity line 17
3. theorem OAI.RyserCoveringCounterexample.exists_slope_of_incidence_infinity_of_ne_vertical line 23
4. theorem OAI.RyserCoveringCounterexample.exists_projectiveTransform_line_to_infinity line 31
5. theorem OAI.RyserCoveringCounterexample.exists_projectiveTransform_direction_to_vertical line 47
6. theorem OAI.RyserCoveringCounterexample.exists_projectiveTransform_direction_frame line 57
7. theorem OAI.RyserCoveringCounterexample.exists_projectiveTransform_normalization line 94
8. theorem OAI.RyserCoveringCounterexample.exists_projective_normalization line 145