OAI/Combinatorics/Crossing/DrawingMarks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.drawingMarks line 11
2. theorem OAI.Zarankiewicz.drawingMarks_finite line 14
3. theorem OAI.Zarankiewicz.crossing_not_vertex line 17
4. theorem OAI.Zarankiewicz.marked_parameters_finite line 23
5. theorem OAI.Zarankiewicz.marked_parameter_zero line 27
6. theorem OAI.Zarankiewicz.marked_parameter_one line 31
7. theorem OAI.Zarankiewicz.unmarked_edge_point_interior line 35
8. theorem OAI.Zarankiewicz.unmarked_intersection_same_edge line 48