OAI/Combinatorics/Crossing/PlanarSegments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.det2 line 13
  2. def OAI.Zarankiewicz.segmentPoint line 15
  3. def OAI.Zarankiewicz.openSegmentTrace line 17
  4. def OAI.Zarankiewicz.SegmentsCrossProperly line 19
  5. def OAI.Zarankiewicz.segmentCrossingSign line 24
  6. theorem OAI.Zarankiewicz.segmentPoint_zero line 28
  7. theorem OAI.Zarankiewicz.segmentPoint_one line 31
  8. theorem OAI.Zarankiewicz.segmentPoint_reverse line 34
  9. theorem OAI.Zarankiewicz.det2_swap line 38
  10. theorem OAI.Zarankiewicz.det2_neg_left line 42
  11. theorem OAI.Zarankiewicz.det2_neg_right line 46
  12. theorem OAI.Zarankiewicz.segment_intersection_parameters_unique line 50