OAI/Combinatorics/Crossing/DrawingSpokePorts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Zarankiewicz.openSegmentTrace_reverse_mem line 9
2. theorem OAI.Zarankiewicz.squaredLength_sub_comm line 14
3. def OAI.Zarankiewicz.PolygonalChain.startPort line 18
4. def OAI.Zarankiewicz.PolygonalChain.endPort line 21
5. theorem OAI.Zarankiewicz.drawing_chain_startPort_interior line 24
6. theorem OAI.Zarankiewicz.drawing_chain_endPort_interior line 34
7. theorem OAI.Zarankiewicz.drawing_chain_startPort_circle line 49
8. theorem OAI.Zarankiewicz.drawing_chain_endPort_circle line 60