OAI/Combinatorics/Crossing/ExteriorSegmentGraph.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.exteriorSegmentGraphline 8 - theorem
OAI.Zarankiewicz.exteriorSegmentGraph_leline 15 - theorem
OAI.Zarankiewicz.graphWalkPath_edge_subset_rangeline 18 - def
OAI.Zarankiewicz.exteriorGraphWalkline 28 - theorem
OAI.Zarankiewicz.exteriorGraphWalk_getVertline 38 - theorem
OAI.Zarankiewicz.exteriorGraphWalk_lengthline 53 - theorem
OAI.Zarankiewicz.exteriorGraphWalk_traceline 58