OAI/Geometry/Cannon/PlaneTopology/Straight.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonEmbeddedArc.Arc.IsStraight line 30
  2. def OAI.CannonEmbeddedArc.Arc.lineArc line 33
  3. lemma OAI.CannonEmbeddedArc.Arc.lineArc_zero line 35
  4. lemma OAI.CannonEmbeddedArc.Arc.lineArc_one line 36
  5. lemma OAI.CannonEmbeddedArc.Arc.lineArc_straight line 37
  6. lemma OAI.CannonEmbeddedArc.Arc.lineArc_range line 39
  7. lemma OAI.CannonEmbeddedArc.Arc.IsStraight.range_eq line 42
  8. lemma OAI.CannonEmbeddedArc.Arc.IsStraight.subarc line 56
  9. lemma OAI.CannonEmbeddedArc.Arc.IsStraight.preimage_convex line 65
  10. theorem OAI.CannonEmbeddedArc.Arc.insert_straight_arrangement line 80
  11. theorem OAI.CannonEmbeddedArc.Arc.straight_arrangement line 126
  12. lemma OAI.CannonTame.connected_in_finite_closed_cover line 155
  13. lemma OAI.CannonEmbeddedArc.Arc.IsStraight.image_Icc line 195
  14. lemma OAI.CannonEmbeddedArc.Arc.range_eq_segment_of_subset line 208
  15. lemma OAI.CannonEmbeddedArc.Arc.Compatible.congr_endpoints_range line 247
  16. lemma OAI.CannonEmbeddedArc.Arc.subarc_in_one_edge line 266
  17. theorem OAI.CannonEmbeddedArc.Arc.arc_in_arrangement_subdivision line 309
  18. theorem OAI.CannonEmbeddedArc.Arc.finite_segment_arc_subdivision line 349
  19. lemma OAI.CannonEmbeddedArc.Arc.consecutive_neighbors line 374
  20. lemma OAI.CannonEmbeddedArc.Arc.consecutive_refinement line 392
  21. lemma OAI.CannonEmbeddedArc.Arc.segment_subarc_image line 407
  22. lemma OAI.CannonEmbeddedArc.Arc.straight_subdivision_refines line 421
  23. lemma OAI.CannonEmbeddedArc.Arc.corner_not_sameRay line 433
  24. theorem OAI.CannonEmbeddedArc.Arc.tame_interior_corner line 462
  25. theorem OAI.CannonEmbeddedArc.Arc.isolate_edge_interior line 488