OAI/Combinatorics/Crossing/InnerDrawingPassages.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Zarankiewicz.DrawingPassages.InnerIndex line 10
  2. def OAI.Zarankiewicz.DrawingPassages.innerMark line 13
  3. def OAI.Zarankiewicz.DrawingPassages.incomingArc line 16
  4. def OAI.Zarankiewicz.DrawingPassages.outgoingArc line 19
  5. def OAI.Zarankiewicz.DrawingPassages.incomingPort line 22
  6. def OAI.Zarankiewicz.DrawingPassages.outgoingPort line 23
  7. theorem OAI.Zarankiewicz.DrawingPassages.incoming_node line 25
  8. theorem OAI.Zarankiewicz.DrawingPassages.outgoing_node line 32
  9. theorem OAI.Zarankiewicz.DrawingPassages.incomingPort_mark line 35
  10. theorem OAI.Zarankiewicz.DrawingPassages.outgoingPort_mark line 41
  11. theorem OAI.Zarankiewicz.DrawingPassages.incomingPort_point line 44
  12. theorem OAI.Zarankiewicz.DrawingPassages.outgoingPort_point line 49
  13. theorem OAI.Zarankiewicz.DrawingPassages.inner_parameter_interior line 52
  14. theorem OAI.Zarankiewicz.DrawingPassages.innerMark_is_crossing line 60
  15. def OAI.Zarankiewicz.DrawingPassages.crossingChord line 68
  16. theorem OAI.Zarankiewicz.DrawingPassages.crossingChord_injective line 72