OAI/Combinatorics/Crossing/PolygonalChains.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.polygonalArcPath line 8
2. structure OAI.Zarankiewicz.PolygonalChain line 13
3. def OAI.Zarankiewicz.PolygonalChain.point line 24
4. def OAI.Zarankiewicz.PolygonalChain.append line 32
5. def OAI.Zarankiewicz.PolygonalChain.path line 46
6. theorem OAI.Zarankiewicz.nonempty_polygonalChain_of_reach line 51
7. theorem OAI.Zarankiewicz.nonempty_polygonalChain_of_path line 59