OAI/Combinatorics/Crossing/ReconnectedWalks.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.surgery_forward_adjline 12 - theorem
OAI.Zarankiewicz.surgery_backward_adjline 16 - def
OAI.Zarankiewicz.reconnectedForwardWalkline 20 - def
OAI.Zarankiewicz.reconnectedBackwardWalkline 26 - theorem
OAI.Zarankiewicz.reconnectedForwardWalk_traceline 32 - theorem
OAI.Zarankiewicz.reconnectedBackwardWalk_traceline 41