OAI/Combinatorics/HalvingLines/PlaneGraph.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.PlaneGraph.height line 10
  2. lemma OAI.PlanarHalving.PlaneGraph.height_left line 13
  3. lemma OAI.PlanarHalving.PlaneGraph.height_right line 14
  4. lemma OAI.PlanarHalving.PlaneGraph.height_point_openSegment line 20
  5. lemma OAI.PlanarHalving.PlaneGraph.height_continuous line 31
  6. lemma OAI.PlanarHalving.PlaneGraph.height_order line 35
  7. def OAI.PlanarHalving.PlaneGraph.Position line 56
  8. structure OAI.PlanarHalving.PlaneGraph.Drawing line 62
  9. def OAI.PlanarHalving.PlaneGraph.Drawing.NonCrossing line 68
  10. lemma OAI.PlanarHalving.PlaneGraph.slope_eq_implies_eq line 73
  11. def OAI.PlanarHalving.PlaneGraph.IsGap line 90
  12. def OAI.PlanarHalving.PlaneGraph.Drawing.gaps line 97
  13. lemma OAI.PlanarHalving.PlaneGraph.height_lt_height_iff line 100
  14. lemma OAI.PlanarHalving.PlaneGraph.height_le_height_iff line 104
  15. def OAI.PlanarHalving.PlaneGraph.InWedge line 108
  16. def OAI.PlanarHalving.PlaneGraph.FirstVertex line 113
  17. lemma OAI.PlanarHalving.PlaneGraph.IsGap.width_pos line 117
  18. lemma OAI.PlanarHalving.PlaneGraph.IsGap.exists_inWedge line 122
  19. lemma OAI.PlanarHalving.PlaneGraph.IsGap.exists_firstVertex line 135
  20. lemma OAI.PlanarHalving.PlaneGraph.IsGap.separated_of_same_source line 148
  21. lemma OAI.PlanarHalving.PlaneGraph.firstVertex_separated_of_source_lt line 183
  22. lemma OAI.PlanarHalving.PlaneGraph.FirstVertex.separated line 207
  23. def OAI.PlanarHalving.PlaneGraph.Drawing.first line 218
  24. lemma OAI.PlanarHalving.PlaneGraph.Drawing.first_spec line 221
  25. def OAI.PlanarHalving.PlaneGraph.Drawing.gapCharge line 224
  26. lemma OAI.PlanarHalving.PlaneGraph.Drawing.gapCharge_injective line 228
  27. lemma OAI.PlanarHalving.PlaneGraph.Drawing.card_gaps_le line 259
  28. lemma OAI.PlanarHalving.PlaneGraph.Drawing.exists_next_gap line 266
  29. def OAI.PlanarHalving.PlaneGraph.Drawing.edgeCharge line 279
  30. lemma OAI.PlanarHalving.PlaneGraph.Drawing.edgeCharge_injective line 286
  31. theorem OAI.PlanarHalving.PlaneGraph.Drawing.planar_bound line 323
  32. lemma OAI.PlanarHalving.PlaneGraph.slope_eq_implies_eq_ne line 333
  33. lemma OAI.PlanarHalving.PlaneGraph.height_of_mem_openSegment line 350
  34. lemma OAI.PlanarHalving.PlaneGraph.openSegment_horizontal_bounds line 365
  35. lemma OAI.PlanarHalving.PlaneGraph.incident_disjoint line 374
  36. def OAI.PlanarHalving.PlaneGraph.Crosses line 387
  37. lemma OAI.PlanarHalving.PlaneGraph.Drawing.crossing_endpoints line 391
  38. def OAI.PlanarHalving.PlaneGraph.edgeIndex line 421
  39. def OAI.PlanarHalving.PlaneGraph.Drawing.crossings line 423
  40. def OAI.PlanarHalving.PlaneGraph.Drawing.uncross line 427
  41. lemma OAI.PlanarHalving.PlaneGraph.Drawing.uncross_nonCrossing line 433
  42. theorem OAI.PlanarHalving.PlaneGraph.Drawing.linear_crossing_bound line 448