OAI/Combinatorics/Crossing/TriangleTransversality.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.TriangleSegmentPositionline 8 - theorem
OAI.Zarankiewicz.triangle_consecutive_roots_neline 14 - theorem
OAI.Zarankiewicz.second_parameter_ne_zeroline 31 - theorem
OAI.Zarankiewicz.second_parameter_ne_oneline 40 - theorem
OAI.Zarankiewicz.triangle_roots_injectiveline 49 - theorem
OAI.Zarankiewicz.triangle_segment_entry_exit_of_positionline 61