OAI/Combinatorics/Crossing/CrossingCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.crossingCoordinates line 10
  2. def OAI.Zarankiewicz.crossingCoordinateInverse line 13
  3. theorem OAI.Zarankiewicz.crossingCoordinates_left_inverse line 15
  4. theorem OAI.Zarankiewicz.crossingCoordinates_right_inverse line 26
  5. theorem OAI.Zarankiewicz.crossingCoordinates_continuous line 37
  6. theorem OAI.Zarankiewicz.crossingCoordinateInverse_continuous line 41
  7. def OAI.Zarankiewicz.crossingCoordinateHomeomorph line 45
  8. def OAI.Zarankiewicz.crossingCoordinateChart line 53
  9. theorem OAI.Zarankiewicz.crossingCoordinates_origin line 71