OAI/Combinatorics/Crossing/FinitePolygonalComposition.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.finitePolygonalChainline 9 - theorem
OAI.Zarankiewicz.finitePolygonalChain_intersection_leftline 14 - theorem
OAI.Zarankiewicz.finitePolygonalChain_intersection_rightline 25 - theorem
OAI.Zarankiewicz.finitePolygonalChain_transverse_leftline 35 - theorem
OAI.Zarankiewicz.finitePolygonalChain_transverse_rightline 44 - theorem
OAI.Zarankiewicz.finitePolygonalChain_intersection_doubleline 50