OAI/Combinatorics/Crossing/SurgeryRouteIntersections.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.PolygonalExterior.reconnectedForwardPath_meeting_otherline 15 - theorem
OAI.Zarankiewicz.PolygonalExterior.reconnectedBackwardPath_meeting_otherline 27 - theorem
OAI.Zarankiewicz.PolygonalExterior.adjacentSurgeryRoutes_meeting_otherline 39 - theorem
OAI.Zarankiewicz.PolygonalExterior.adjacentSurgeryRoutes_meeting_each_otherline 59