OAI/Combinatorics/Crossing/AxisFiniteCrossings.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Zarankiewicz.axis_open_intersection_subsingleton line 10
2. theorem OAI.Zarankiewicz.axis_intercept_pair_ne line 20
3. theorem OAI.Zarankiewicz.axisContinuousDrawing_pair_subsingleton line 26
4. theorem OAI.Zarankiewicz.axisContinuousDrawing_crossings_finite line 34
5. theorem OAI.Zarankiewicz.axisContinuousDrawing_crossings_proper line 51