OAI/Combinatorics/Ryser/Geometry/Basic.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RyserCoveringCounterexample.Point line 12
  2. abbrev OAI.RyserCoveringCounterexample.Direction line 13
  3. abbrev OAI.RyserCoveringCounterexample.AffineLine line 14
  4. abbrev OAI.RyserCoveringCounterexample.ProjectivePoint line 15
  5. abbrev OAI.RyserCoveringCounterexample.ProjectiveLine line 16
  6. def OAI.RyserCoveringCounterexample.projection line 20
  7. def OAI.RyserCoveringCounterexample.Incidence line 24
  8. instance OAI.RyserCoveringCounterexample.(instance at line 27) line 27
  9. def OAI.RyserCoveringCounterexample.lineThrough line 31
  10. theorem OAI.RyserCoveringCounterexample.projection_none line 34
  11. theorem OAI.RyserCoveringCounterexample.projection_some line 35
  12. theorem OAI.RyserCoveringCounterexample.projection_some_zero line 37
  13. theorem OAI.RyserCoveringCounterexample.incidence_mk line 40
  14. theorem OAI.RyserCoveringCounterexample.lineThrough_direction line 43
  15. theorem OAI.RyserCoveringCounterexample.lineThrough_offset line 45
  16. theorem OAI.RyserCoveringCounterexample.incidence_lineThrough line 47
  17. theorem OAI.RyserCoveringCounterexample.incidence_lineThrough_iff line 50
  18. theorem OAI.RyserCoveringCounterexample.lineThrough_eq_iff line 53
  19. theorem OAI.RyserCoveringCounterexample.eq_lineThrough_of_incidence line 57
  20. theorem OAI.RyserCoveringCounterexample.point_eq_of_projection_axes line 63
  21. theorem OAI.RyserCoveringCounterexample.projection_add line 69
  22. theorem OAI.RyserCoveringCounterexample.projection_sub line 75
  23. theorem OAI.RyserCoveringCounterexample.projection_mul line 81
  24. def OAI.RyserCoveringCounterexample.ProjectiveIncidence line 87
  25. instance OAI.RyserCoveringCounterexample.(instance at line 93) line 93
  26. theorem OAI.RyserCoveringCounterexample.projectiveIncidence_finite_affine line 97
  27. theorem OAI.RyserCoveringCounterexample.projectiveIncidence_infinite_affine line 99
  28. theorem OAI.RyserCoveringCounterexample.projectiveIncidence_finite_infinity line 101
  29. theorem OAI.RyserCoveringCounterexample.projectiveIncidence_infinite_infinity line 103
  30. def OAI.RyserCoveringCounterexample.linePoints line 109
  31. def OAI.RyserCoveringCounterexample.affinePencil line 112
  32. def OAI.RyserCoveringCounterexample.projectiveLinePoints line 115
  33. def OAI.RyserCoveringCounterexample.projectivePencil line 118
  34. theorem OAI.RyserCoveringCounterexample.mem_linePoints line 121
  35. theorem OAI.RyserCoveringCounterexample.mem_affinePencil line 125
  36. theorem OAI.RyserCoveringCounterexample.mem_projectiveLinePoints line 129
  37. theorem OAI.RyserCoveringCounterexample.mem_projectivePencil line 133