OAI/Combinatorics/Crossing/ReplaceDrawingEdges.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.ContinuousDrawing.replaceTwoRoutesline 9 - theorem
OAI.Zarankiewicz.ContinuousDrawing.replaceTwoRoutes_firstline 20 - theorem
OAI.Zarankiewicz.ContinuousDrawing.replaceTwoRoutes_secondline 26 - theorem
OAI.Zarankiewicz.ContinuousDrawing.replaceTwoRoutes_otherline 32 - def
OAI.Zarankiewicz.ContinuousDrawing.replaceTwoEdgesline 39