OAI/Combinatorics/Crossing/ChainTracePieces.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.PolygonalChain.piece_subset_path_rangeline 9 - theorem
OAI.Zarankiewicz.drawing_chain_range_eqline 14 - theorem
OAI.Zarankiewicz.drawing_chain_pieces_posline 20