OAI/Combinatorics/Crossing/AdjacentSurgeryDrawing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.adjacentSurgeryDrawing line 11
  2. theorem OAI.Zarankiewicz.adjacentSurgeryDrawing_vertex line 22
  3. theorem OAI.Zarankiewicz.adjacentSurgeryDrawing_first line 28
  4. theorem OAI.Zarankiewicz.adjacentSurgeryDrawing_second line 35
  5. theorem OAI.Zarankiewicz.adjacentSurgeryDrawing_other line 42
  6. theorem OAI.Zarankiewicz.adjacentSurgeryRouteP_hasFiniteAffineCover line 50
  7. theorem OAI.Zarankiewicz.adjacentSurgeryRouteQ_hasFiniteAffineCover line 59