OAI/Combinatorics/Crossing/ReconnectedPaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.reconnectedForwardPath line 11
2. def OAI.Zarankiewicz.reconnectedBackwardPath line 16
3. theorem OAI.Zarankiewicz.reconnectedForwardPath_injective line 21
4. theorem OAI.Zarankiewicz.reconnectedBackwardPath_injective line 28
5. theorem OAI.Zarankiewicz.reconnectedForwardPath_hasFiniteAffineCover line 35
6. theorem OAI.Zarankiewicz.reconnectedBackwardPath_hasFiniteAffineCover line 41
7. theorem OAI.Zarankiewicz.reconnectedForwardPath_trace line 47
8. theorem OAI.Zarankiewicz.reconnectedBackwardPath_trace line 57