OAI/Combinatorics/Crossing/PolygonalChainComposition.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.PolygonalChain.reverseline 11 - theorem
OAI.Zarankiewicz.PolygonalChain.intersection_join_leftline 25 - theorem
OAI.Zarankiewicz.PolygonalChain.intersection_join_rightline 31 - theorem
OAI.Zarankiewicz.PolygonalChain.intersection_reverse_leftline 37 - theorem
OAI.Zarankiewicz.PolygonalChain.intersection_reverse_rightline 41