OAI/Combinatorics/Crossing/DrawingSubdivisionGraph.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.drawingSubdivisionGraphline 9 - theorem
OAI.Zarankiewicz.drawingSubdivisionGraph_piece_adjline 21 - theorem
OAI.Zarankiewicz.common_endpoint_alternativesline 26 - theorem
OAI.Zarankiewicz.drawingSubdivisionGraph_embeddingline 34 - theorem
OAI.Zarankiewicz.drawingSubdivisionGraph_finite_supportline 65