OAI/Combinatorics/Crossing/PolygonalChainShortcuts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.PolygonalChain.withEndpoints line 9
2. theorem OAI.Zarankiewicz.PolygonalChain.minimum_shortcut_bound line 18
3. theorem OAI.Zarankiewicz.PolygonalChain.minimum_vertices_ne line 26
4. theorem OAI.Zarankiewicz.PolygonalChain.minimum_nonadjacent_disjoint line 35
5. theorem OAI.Zarankiewicz.PolygonalChain.minimum_two_step_not_subset line 54