OAI/Combinatorics/Crossing/TruncatedSpokeCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Zarankiewicz.TruncatedSpokeCoordinates line 10
  2. theorem OAI.Zarankiewicz.nonempty_truncatedSpokeCoordinates line 18
  3. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedPort line 30
  4. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.tangentPort line 34
  5. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.tangentPort_eq line 37
  6. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedPort_level line 46
  7. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.shiftedPort_circle line 54
  8. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.connector_strictly_outside line 61
  9. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.exists_vertex_average_radius line 70