OAI/Combinatorics/HalvingLines/Chains.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.PlaneGraph.Drawing.NoMultiple line 11
  2. lemma OAI.PlanarHalving.PlaneGraph.Drawing.crossing_props line 18
  3. def OAI.PlanarHalving.PlaneGraph.Drawing.crossingPoint line 25
  4. lemma OAI.PlanarHalving.PlaneGraph.Drawing.crossingPoint_mem line 28
  5. lemma OAI.PlanarHalving.PlaneGraph.Drawing.crossingPoint_injective line 33
  6. lemma OAI.PlanarHalving.PlaneGraph.Drawing.crossing_slopes_ne line 62
  7. structure OAI.PlanarHalving.PlaneGraph.ConvexCover line 84
  8. structure OAI.PlanarHalving.PlaneGraph.ConcaveCover line 89
  9. lemma OAI.PlanarHalving.PlaneGraph.height_difference line 96
  10. lemma OAI.PlanarHalving.PlaneGraph.ConvexCover.crossing_support line 100
  11. lemma OAI.PlanarHalving.PlaneGraph.ConvexCover.crossing_eq_of_x line 117
  12. lemma OAI.PlanarHalving.PlaneGraph.ConvexCover.crossing_sign_injective line 133
  13. theorem OAI.PlanarHalving.PlaneGraph.ConvexCover.crossing_bound line 161
  14. def OAI.PlanarHalving.Batches.System.edges line 176
  15. lemma OAI.PlanarHalving.Batches.System.mem_edges line 179
  16. lemma OAI.PlanarHalving.Batches.System.batch_unique line 183
  17. lemma OAI.PlanarHalving.Batches.System.card_edges line 201
  18. def OAI.PlanarHalving.Batches.System.vertices line 210
  19. lemma OAI.PlanarHalving.Batches.System.edge_ends line 213
  20. def OAI.PlanarHalving.Batches.System.drawing line 218
  21. structure OAI.PlanarHalving.Batches.System.EdgeTrace line 224
  22. lemma OAI.PlanarHalving.Batches.System.trace_exists line 233
  23. def OAI.PlanarHalving.Batches.System.trace line 247
  24. lemma OAI.PlanarHalving.Batches.System.token_fixed_of_outside line 251
  25. lemma OAI.PlanarHalving.Batches.System.trace_token_mem line 265
  26. def OAI.PlanarHalving.Batches.System.convexOwner line 272
  27. lemma OAI.PlanarHalving.Batches.System.convexOwner_eq line 276
  28. lemma OAI.PlanarHalving.Batches.System.convexOwner_mem line 281
  29. def OAI.PlanarHalving.Batches.System.convexCover line 287
  30. theorem OAI.PlanarHalving.PlaneGraph.ConvexCover.crossing_bound_finset line 316
  31. lemma OAI.PlanarHalving.PlaneGraph.slope_neg_reverse line 338
  32. lemma OAI.PlanarHalving.PlaneGraph.height_neg_reverse line 342