OAI/Combinatorics/Crossing/TruncatedChainVertices.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Zarankiewicz.radialPort_parameter_half line 8
2. def OAI.Zarankiewicz.PolygonalChain.startFraction line 19
3. def OAI.Zarankiewicz.PolygonalChain.endFraction line 22
4. def OAI.Zarankiewicz.PolygonalChain.truncatedVertices line 25
5. theorem OAI.Zarankiewicz.PolygonalChain.startPort_eq_fraction line 28
6. theorem OAI.Zarankiewicz.PolygonalChain.endPort_eq_fraction line 31
7. theorem OAI.Zarankiewicz.PolygonalChain.truncatedVertices_first line 37
8. theorem OAI.Zarankiewicz.PolygonalChain.truncatedVertices_last line 40
9. theorem OAI.Zarankiewicz.PolygonalChain.truncated_piece_subset line 43