OAI/Combinatorics/Crossing/SegmentSides.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.orient2 line 8
2. theorem OAI.Zarankiewicz.orient2_self_segment line 10
3. theorem OAI.Zarankiewicz.orient2_segment line 14
4. theorem OAI.Zarankiewicz.orient2_difference line 19
5. theorem OAI.Zarankiewicz.orient2_other_difference line 24
6. theorem OAI.Zarankiewicz.segmentCrossingSign_of_positive_sides line 29
7. theorem OAI.Zarankiewicz.not_segmentsCrossProperly_of_same_side line 45