OAI/Combinatorics/Crossing/DrawingDeletion.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.deleteRightVertexline 10 - theorem
OAI.Zarankiewicz.crossing_survives_deletion_iffline 13 - theorem
OAI.Zarankiewicz.crossing_columns_neline 43 - theorem
OAI.Zarankiewicz.two_excluded_indicesline 52 - theorem
OAI.Zarankiewicz.crossing_deletion_multiplicityline 62