OAI/Combinatorics/HalvingLines/ChainDrawing.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.Batches.System.flip line 11
  2. lemma OAI.PlanarHalving.Batches.System.flip_loss line 34
  3. lemma OAI.PlanarHalving.Batches.System.flip_gain line 39
  4. lemma OAI.PlanarHalving.Batches.System.flip_edge line 45
  5. lemma OAI.PlanarHalving.Batches.System.flip_vertices line 50
  6. def OAI.PlanarHalving.Batches.System.concaveCover line 62
  7. lemma OAI.PlanarHalving.Batches.System.concaveOwner_mem line 79
  8. theorem OAI.PlanarHalving.Batches.System.crossing_cap line 85
  9. def OAI.PlanarHalving.PlaneGraph.sortEdge line 99
  10. lemma OAI.PlanarHalving.PlaneGraph.sortEdge_order line 102
  11. lemma OAI.PlanarHalving.PlaneGraph.sortEdge_cases line 109
  12. lemma OAI.PlanarHalving.PlaneGraph.sortEdge_coincide line 113
  13. lemma OAI.PlanarHalving.PlaneGraph.Drawing.sortEdge_injective line 121
  14. lemma OAI.PlanarHalving.PlaneGraph.openSegment_sortEdge line 131
  15. lemma OAI.PlanarHalving.PlaneGraph.segment_sortEdge line 139
  16. lemma OAI.PlanarHalving.PlaneGraph.Drawing.noMultiple_of_generic line 147
  17. lemma OAI.PlanarHalving.PlaneGraph.Generic.position line 159
  18. lemma OAI.PlanarHalving.PlaneGraph.Generic.x_injective line 160
  19. def OAI.PlanarHalving.PlaneGraph.Drawing.restrictEdges line 170
  20. lemma OAI.PlanarHalving.PlaneGraph.Drawing.restrict_crossings line 178
  21. lemma OAI.PlanarHalving.Batches.System.vertices_le line 192
  22. theorem OAI.PlanarHalving.Batches.System.localized_crossing line 195
  23. theorem OAI.PlanarHalving.Batches.System.cubed_bound line 221
  24. lemma OAI.PlanarHalving.PlaneGraph.height_of_mem_segment line 249
  25. def OAI.PlanarHalving.RankCoordinates.envelope line 262
  26. lemma OAI.PlanarHalving.RankCoordinates.le_envelope line 266
  27. lemma OAI.PlanarHalving.RankCoordinates.envelope_le line 270
  28. lemma OAI.PlanarHalving.RankCoordinates.envelope_attains line 274
  29. lemma OAI.PlanarHalving.RankCoordinates.continuous_envelope line 279
  30. lemma OAI.PlanarHalving.RankCoordinates.convexOn_envelope line 287
  31. lemma OAI.PlanarHalving.RankCoordinates.envelope_slopes line 302
  32. lemma OAI.PlanarHalving.Batches.ConvexPath.lower_ray line 325
  33. lemma OAI.PlanarHalving.Batches.ConvexPath.upper_ray line 340
  34. def OAI.PlanarHalving.Batches.ConvexPath.extensionSlopes line 355
  35. def OAI.PlanarHalving.Batches.ConvexPath.extensionIntercepts line 360
  36. def OAI.PlanarHalving.Batches.ConvexPath.extension line 366
  37. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_slopes line 369
  38. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_below_vertex line 382
  39. lemma OAI.PlanarHalving.Batches.ConvexPath.extension_edge line 401