OAI/Combinatorics/Crossing/BalancedAxisDrawing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Zarankiewicz.BalancedAxisRealization line 9
  2. theorem OAI.Zarankiewicz.nonempty_balancedAxisRealization line 18
  3. theorem OAI.Zarankiewicz.BalancedAxisRealization.vertical_injective line 36
  4. theorem OAI.Zarankiewicz.BalancedAxisRealization.horizontal_injective line 37
  5. theorem OAI.Zarankiewicz.BalancedAxisRealization.vertical_ne_zero line 38
  6. theorem OAI.Zarankiewicz.BalancedAxisRealization.horizontal_ne_zero line 39
  7. theorem OAI.Zarankiewicz.BalancedAxisRealization.vertical_abs_strictMono line 40
  8. theorem OAI.Zarankiewicz.BalancedAxisRealization.horizontal_abs_strictMono line 41
  9. def OAI.Zarankiewicz.BalancedAxisRealization.drawing line 43
  10. theorem OAI.Zarankiewicz.BalancedAxisRealization.drawing_noAdjacent line 47
  11. theorem OAI.Zarankiewicz.BalancedAxisRealization.drawing_vertex_left line 50
  12. theorem OAI.Zarankiewicz.BalancedAxisRealization.drawing_vertex_right line 51
  13. theorem OAI.Zarankiewicz.BalancedAxisRealization.drawing_edge line 52
  14. theorem OAI.Zarankiewicz.BalancedAxisRealization.drawing_edgeInterior line 55
  15. theorem OAI.Zarankiewicz.exists_axis_admissible line 62