OAI/Combinatorics/CompleteCrossing/Normalization.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Reorientation invariance and normalization without adjacent crossings or crossing knots.

  1. def OAI.Paper170.Graph.reorient line 21
  2. theorem OAI.Paper170.unitInterval_symm_mem_Ioo line 33
  3. def OAI.Paper170.ContinuousDrawing.reorientedPath line 41
  4. theorem OAI.Paper170.ContinuousDrawing.reorientedPath_apply line 48
  5. def OAI.Paper170.ContinuousDrawing.reorient line 54
  6. theorem OAI.Paper170.ContinuousDrawing.reorient_edgeInterior line 75
  7. theorem OAI.Paper170.ContinuousDrawing.reorient_crossingPoints line 98
  8. def OAI.Paper170.AdmissibleDrawing.reorient line 108
  9. theorem OAI.Paper170.AdmissibleDrawing.reorient_crossingCount line 122
  10. theorem OAI.Paper170.Graph.eq_of_endpoints line 142
  11. theorem OAI.Paper170.Graph.reorient_reorient line 150
  12. def OAI.Paper170.AdmissibleDrawing.castGraph line 161
  13. theorem OAI.Paper170.AdmissibleDrawing.castGraph_crossingCount line 163
  14. theorem OAI.Paper170.AdmissibleDrawing.reorient_minimal line 168
  15. def OAI.Paper170.reparametrizedContinuous line 191
  16. lemma OAI.Paper170.reparametrized_interior line 208
  17. lemma OAI.Paper170.reparametrized_crossings line 228
  18. def OAI.Paper170.reparametrizedDrawing line 237
  19. lemma OAI.Paper170.reparametrized_count line 255
  20. lemma OAI.Paper170.normalized_of_locally_straight line 268
  21. theorem OAI.Paper170Geometry.PolygonalExterior.assembled_locallyStraightCrossings line 320
  22. theorem OAI.Paper170Geometry.minimum_no_common_source_or_target line 363
  23. theorem OAI.Paper170Geometry.minimum_no_adjacent line 391
  24. theorem OAI.Paper170Geometry.exists_minimum_assembled line 416
  25. theorem OAI.Paper170Geometry.polygonal_no_adjacent_locally_straight line 439
  26. theorem OAI.Paper170.polygonal_no_adjacent_normalization line 458
  27. theorem OAI.Paper170.normalized_minimum_exists line 465