OAI/Combinatorics/BalancedRyser/Incidence/AffineIncidence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.onLine_lineThrough line 11
  2. theorem OAI.Balanced.lineThrough_direction line 14
  3. theorem OAI.Balanced.line_eq_lineThrough line 17
  4. theorem OAI.Balanced.eq_of_onLine_same_direction line 23
  5. theorem OAI.Balanced.eq_of_two_common_points line 27
  6. theorem OAI.Balanced.common_point_eq_of_lines_ne line 64
  7. def OAI.Balanced.linePointsEquiv line 70
  8. theorem OAI.Balanced.onLine_lineIntersection_left line 95
  9. theorem OAI.Balanced.onLine_lineIntersection_right line 109
  10. def OAI.Balanced.evalPairEquiv line 127
  11. theorem OAI.Balanced.onLine_joiningLine_left line 147
  12. theorem OAI.Balanced.onLine_joiningLine_right line 152
  13. theorem OAI.Balanced.existsUnique_line_of_ne line 164
  14. def OAI.Balanced.linesThroughEquiv line 178
  15. theorem OAI.Balanced.card_lines_through line 186
  16. theorem OAI.Balanced.linePoints_card line 192
  17. theorem OAI.Balanced.linePoints_inter_card_le_one line 197
  18. theorem OAI.Balanced.parallel_linePoints_disjoint line 205