OAI/Combinatorics/Crossing/TruncatedSignedIntersections.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.VertexTruncation.piece_subset_rangeline 11 - def
OAI.Zarankiewicz.VertexTruncation.signedIntersectionline 16 - theorem
OAI.Zarankiewicz.VertexTruncation.signedIntersection_selfline 19 - theorem
OAI.Zarankiewicz.VertexTruncation.signedIntersection_swapline 22 - theorem
OAI.Zarankiewicz.VertexTruncation.signedIntersection_zero_of_pairCrossings_emptyline 29 - theorem
OAI.Zarankiewicz.VertexTruncation.pairCrossings_pos_of_signedIntersection_ne_zeroline 64 - theorem
OAI.Zarankiewicz.VertexTruncation.signedIntersection_adjacent_zeroline 71