OAI/Combinatorics/Crossing/DrawingRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.restrictEdge line 10
2. def OAI.Zarankiewicz.restrictContinuousDrawing line 13
3. theorem OAI.Zarankiewicz.restrict_edgeInterior line 21
4. theorem OAI.Zarankiewicz.restrict_crossingPoints_subset line 25
5. def OAI.Zarankiewicz.restrictDrawing line 30
6. theorem OAI.Zarankiewicz.crossingCount_restrict_le line 39
7. theorem OAI.Zarankiewicz.restrict_noAdjacentCrossings line 47