OAI/Combinatorics/Crossing/TruncatedChainDirections.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.PolygonalChain.truncatedScale line 9
2. theorem OAI.Zarankiewicz.PolygonalChain.truncated_start_formula line 12
3. theorem OAI.Zarankiewicz.PolygonalChain.truncated_end_formula line 20
4. theorem OAI.Zarankiewicz.PolygonalChain.truncated_direction line 29
5. theorem OAI.Zarankiewicz.PolygonalChain.truncatedScale_pos line 35
6. theorem OAI.Zarankiewicz.PolygonalChain.truncated_direction_ne_zero line 46