OAI/Combinatorics/Crossing/MinimumChainGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Zarankiewicz.adjacent_segments_meet_only_at_bend line 9
2. theorem OAI.Zarankiewicz.PolygonalChain.minimum_piece_ne_zero line 25
3. theorem OAI.Zarankiewicz.PolygonalChain.minimum_bend_det_ne_zero line 30
4. theorem OAI.Zarankiewicz.PolygonalChain.minimum_adjacent_intersection line 39