OAI/Combinatorics/Crossing/RetainedDrawingArcs.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Zarankiewicz.DrawingPassages.ArcIndex line 11
  2. theorem OAI.Zarankiewicz.DrawingPassages.node_mark line 13
  3. def OAI.Zarankiewicz.DrawingPassages.arcStartMark line 19
  4. def OAI.Zarankiewicz.DrawingPassages.arcEndMark line 22
  5. def OAI.Zarankiewicz.DrawingPassages.arcStart line 25
  6. def OAI.Zarankiewicz.DrawingPassages.arcEnd line 28
  7. def OAI.Zarankiewicz.DrawingPassages.arc line 31
  8. theorem OAI.Zarankiewicz.DrawingPassages.arc_gap line 34
  9. theorem OAI.Zarankiewicz.DrawingPassages.arc_injective line 38
  10. theorem OAI.Zarankiewicz.DrawingPassages.arc_endpoints_ne line 41
  11. theorem OAI.Zarankiewicz.DrawingPassages.arc_range line 45
  12. theorem OAI.Zarankiewicz.DrawingPassages.arc_avoids_marks line 49
  13. theorem OAI.Zarankiewicz.DrawingPassages.retained_parameter_outside line 58
  14. theorem OAI.Zarankiewicz.DrawingPassages.arc_interior_outside line 85
  15. theorem OAI.Zarankiewicz.DrawingPassages.arc_start_on_circle line 90
  16. theorem OAI.Zarankiewicz.DrawingPassages.arc_end_on_circle line 95