OAI/Combinatorics/Crossing/OrderedExteriorPaths.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.DrawingPassages.orderedArc line 12
  2. theorem OAI.Zarankiewicz.DrawingPassages.orderedArc_val line 15
  3. theorem OAI.Zarankiewicz.DrawingPassages.orderedArc_inj line 20
  4. theorem OAI.Zarankiewicz.DrawingPassages.orderedArc_first line 26
  5. theorem OAI.Zarankiewicz.DrawingPassages.orderedArc_last line 30
  6. def OAI.Zarankiewicz.DrawingPassages.orderedInner line 34
  7. theorem OAI.Zarankiewicz.DrawingPassages.orderedInner_incoming line 38
  8. theorem OAI.Zarankiewicz.DrawingPassages.orderedInner_outgoing line 47
  9. theorem OAI.Zarankiewicz.DrawingPassages.orderedInner_inj line 56
  10. def OAI.Zarankiewicz.PolygonalExterior.orderedPath line 66
  11. def OAI.Zarankiewicz.PolygonalExterior.orderedBridge line 70
  12. theorem OAI.Zarankiewicz.PolygonalExterior.orderedBridge_apply line 73
  13. theorem OAI.Zarankiewicz.PolygonalExterior.orderedBridge_range line 85
  14. def OAI.Zarankiewicz.PolygonalExterior.middlePath line 91