OAI/Combinatorics/CompleteCrossing/CirclePlacement.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Generic circular placement, prescribed arcs, restrictions, and existence of drawings.

  1. def OAI.Paper170.completeEdgeOf line 22
  2. theorem OAI.Paper170.completeEdgeOf_endpoints line 26
  3. theorem OAI.Paper170.completeEdgeOf_injective line 34
  4. theorem OAI.Paper170.unitInterval_symm_mem_open line 50
  5. theorem OAI.Paper170.path_symm_open_image line 57
  6. def OAI.Paper170.restrictedCompletePath line 68
  7. theorem OAI.Paper170.restrictedCompletePath_injective line 91
  8. theorem OAI.Paper170.restrictedCompletePath_interior line 109
  9. theorem OAI.Paper170.restrictedCompletePath_avoids line 130
  10. def OAI.Paper170.restrictedCompleteContinuous line 141
  11. theorem OAI.Paper170.restrictedComplete_edgeInterior line 149
  12. theorem OAI.Paper170.restrictedComplete_crossings_subset line 155
  13. def OAI.Paper170.restrictedCompleteAdmissible line 162
  14. def OAI.Paper170.circleConcurrency line 188
  15. def OAI.Paper170.circleLine line 192
  16. theorem OAI.Paper170.circleLine_param line 195
  17. theorem OAI.Paper170.circleLine_chord line 201
  18. theorem OAI.Paper170.circleConcurrency_of_lines line 211
  19. def OAI.Paper170.circleConcurrencyPolynomial line 222
  20. theorem OAI.Paper170.circleConcurrencyPolynomial_eval line 227
  21. theorem OAI.Paper170.circleConcurrencyPolynomial_ne_zero line 232
  22. theorem OAI.Paper170.circle_configuration_exists line 243
  23. lemma OAI.Paper170.circle_differencePolynomial_ne_zero line 312
  24. lemma OAI.Paper170.circle_antipodalPolynomial_ne_zero line 318
  25. theorem OAI.Paper170.exists_generic_circle_parameters line 324
  26. lemma OAI.Paper170.circlePoint_add_ne_zero line 361
  27. lemma OAI.Paper170.circleParameters_no_triples line 393
  28. theorem OAI.Paper170.exists_circle_points_in_parameter_intervals line 423
  29. lemma OAI.Paper170.continuous_circle_similarity line 438
  30. lemma OAI.Paper170.circle_similarity_add line 452
  31. lemma OAI.Paper170.circle_similarity_zero line 457
  32. lemma OAI.Paper170.circle_similarity_no_triples line 460
  33. theorem OAI.Paper170.exists_generic_circle_points_in_neighborhoods line 489
  34. theorem OAI.Paper170.exists_generic_circle_points_in_disjoint_arcs line 539
  35. theorem OAI.Paper170.exists_circle_configuration_in_parameter_arcs line 558
  36. theorem OAI.Paper170.admissible_drawing_exists line 611
  37. theorem OAI.Paper170.minimum_drawing_exists line 615