OAI/Combinatorics/Crossing/BipartiteDartGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.forwardBipartiteDart line 10
  2. def OAI.Zarankiewicz.backwardBipartiteDart line 13
  3. def OAI.Zarankiewicz.bipartiteDartEdge line 16
  4. def OAI.Zarankiewicz.bipartiteDartSign line 24
  5. theorem OAI.Zarankiewicz.bipartiteDart_cases line 29
  6. theorem OAI.Zarankiewicz.bipartiteDart_source_incident line 38
  7. theorem OAI.Zarankiewicz.bipartiteDart_target_incident line 44
  8. def OAI.Zarankiewicz.dartSourceIncident line 50
  9. def OAI.Zarankiewicz.dartTargetIncident line 53
  10. theorem OAI.Zarankiewicz.bipartiteDartEdge_symm line 56
  11. theorem OAI.Zarankiewicz.bipartiteDartSign_symm line 60
  12. theorem OAI.Zarankiewicz.orientedEdgeStep_dart line 66