OAI/Combinatorics/Crossing/DartCyclePaths.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.incidentCast line 10
  2. theorem OAI.Zarankiewicz.incidentCast_val line 13
  3. def OAI.Zarankiewicz.dartPassageNext line 16
  4. theorem OAI.Zarankiewicz.dartPassage_ne line 20
  5. theorem OAI.Zarankiewicz.VertexTruncation.spokePort_cast line 30
  6. def OAI.Zarankiewicz.VertexTruncation.dartCycleVertex line 33
  7. def OAI.Zarankiewicz.VertexTruncation.dartCycleBlock line 36
  8. def OAI.Zarankiewicz.VertexTruncation.dartCycleChain line 43
  9. def OAI.Zarankiewicz.VertexTruncation.graphCycleChain line 49
  10. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedPort_cast line 58
  11. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedCycleVertex line 61
  12. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedCycleBlock line 64
  13. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedCycleChain line 71
  14. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedGraphCycleChain line 77