OAI/Combinatorics/HalvingLines/Perturbation.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.Perturbation.orient_cycle line 10
  2. lemma OAI.PlanarHalving.Perturbation.orient_segment line 12
  3. lemma OAI.PlanarHalving.Perturbation.no_vertex_openSegment line 18
  4. lemma OAI.PlanarHalving.Perturbation.two_lines_intersection line 26
  5. lemma OAI.PlanarHalving.Perturbation.slope_eq_orient_zero line 37
  6. def OAI.PlanarHalving.Perturbation.intercept line 45
  7. def OAI.PlanarHalving.Perturbation.intersectionPoint line 46
  8. lemma OAI.PlanarHalving.Perturbation.orient_line_eq line 50
  9. lemma OAI.PlanarHalving.Perturbation.intersectionPoint_eq line 57
  10. abbrev OAI.PlanarHalving.Perturbation.Edge line 71
  11. def OAI.PlanarHalving.Perturbation.edgeSlope line 73
  12. def OAI.PlanarHalving.Perturbation.onLine line 74
  13. structure OAI.PlanarHalving.Perturbation.Regular line 76
  14. lemma OAI.PlanarHalving.Perturbation.Regular.generic line 83
  15. def OAI.PlanarHalving.Perturbation.newEdge line 97
  16. def OAI.PlanarHalving.Perturbation.oldEdge line 98
  17. lemma OAI.PlanarHalving.Perturbation.newEdge_injective line 100
  18. lemma OAI.PlanarHalving.Perturbation.oldEdge_injective line 103
  19. lemma OAI.PlanarHalving.Perturbation.newEdge_ne_oldEdge line 108
  20. lemma OAI.PlanarHalving.Perturbation.edge_cases line 112
  21. lemma OAI.PlanarHalving.Perturbation.edgeSlope_new line 121
  22. lemma OAI.PlanarHalving.Perturbation.edgeSlope_old line 123
  23. lemma OAI.PlanarHalving.Perturbation.onLine_new line 125
  24. lemma OAI.PlanarHalving.Perturbation.onLine_old line 127
  25. lemma OAI.PlanarHalving.Perturbation.open_dense_affine line 134
  26. lemma OAI.PlanarHalving.Perturbation.open_dense_orient line 151
  27. lemma OAI.PlanarHalving.Perturbation.open_dense_forall line 165
  28. lemma OAI.PlanarHalving.Perturbation.open_dense_and line 172
  29. def OAI.PlanarHalving.Perturbation.edgeMeet line 177
  30. def OAI.PlanarHalving.Perturbation.Fresh line 180
  31. lemma OAI.PlanarHalving.Perturbation.fresh_open_dense line 186
  32. lemma OAI.PlanarHalving.Perturbation.Fresh.xdistinct line 223
  33. lemma OAI.PlanarHalving.Perturbation.Fresh.general line 233
  34. lemma OAI.PlanarHalving.Perturbation.Fresh.slopes line 260
  35. lemma OAI.PlanarHalving.Perturbation.Fresh.two_new line 283
  36. lemma OAI.PlanarHalving.Perturbation.Fresh.one_new line 291
  37. lemma OAI.PlanarHalving.Perturbation.Fresh.regular line 303
  38. lemma OAI.PlanarHalving.Perturbation.regular_empty line 330
  39. lemma OAI.PlanarHalving.Perturbation.regular_approx line 339
  40. lemma OAI.PlanarHalving.Perturbation.dense_regular line 356
  41. lemma OAI.PlanarHalving.Perturbation.dense_generic line 362
  42. lemma OAI.PlanarHalving.Perturbation.generic_same_sides line 365
  43. lemma OAI.PlanarHalving.Perturbation.generic_same_halvingCount line 399