OAI/Combinatorics/Crossing/SubdivisionSegments.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.PolygonalParametrization.pieceTraceline 9 - theorem
OAI.Zarankiewicz.PolygonalParametrization.pieceTrace_parameterline 12 - theorem
OAI.Zarankiewicz.PolygonalParametrization.pieceTrace_subset_rangeline 20 - theorem
OAI.Zarankiewicz.PolygonalParametrization.pieceTrace_knot_endpointline 26 - theorem
OAI.Zarankiewicz.PolygonalParametrization.pieceTrace_other_piece_endpointline 45 - theorem
OAI.Zarankiewicz.subdivision_mark_endpointline 75