OAI/Combinatorics/Crossing/SegmentTraversalReversal.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.segmentPairTransverse_of_not_meetline 9 - theorem
OAI.Zarankiewicz.segmentCrossingSign_eq_zero_of_not_meetline 14 - theorem
OAI.Zarankiewicz.segmentPairTransverse_reverse_leftline 19 - theorem
OAI.Zarankiewicz.segmentPairTransverse_reverse_rightline 30 - theorem
OAI.Zarankiewicz.PolygonalChain.transverse_reverse_leftline 38 - theorem
OAI.Zarankiewicz.PolygonalChain.transverse_reverse_rightline 48