OAI/Geometry/Cannon/PlaneTopology/Arc.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Embedded arcs and compatible finite subdivisions.

  1. structure OAI.CannonEmbeddedArc.Arc line 15
  2. instance OAI.CannonEmbeddedArc.(instance at line 20) line 20
  3. lemma OAI.CannonEmbeddedArc.Arc.continuous line 23
  4. lemma OAI.CannonEmbeddedArc.Arc.compact_range line 24
  5. lemma OAI.CannonEmbeddedArc.Arc.endpoints_ne line 25
  6. def OAI.CannonEmbeddedArc.Arc.path line 29
  7. lemma OAI.CannonEmbeddedArc.Arc.path_apply line 32
  8. def OAI.CannonEmbeddedArc.Arc.subarc line 34
  9. lemma OAI.CannonEmbeddedArc.Arc.subarc_zero line 46
  10. lemma OAI.CannonEmbeddedArc.Arc.subarc_one line 48
  11. lemma OAI.CannonEmbeddedArc.Arc.subarc_range_subset line 50
  12. def OAI.CannonEmbeddedArc.Arc.spliceFun line 55
  13. lemma OAI.CannonEmbeddedArc.Arc.spliceFun_left line 58
  14. lemma OAI.CannonEmbeddedArc.Arc.spliceFun_right line 60
  15. lemma OAI.CannonEmbeddedArc.Arc.continuous_spliceFun line 68
  16. def OAI.CannonEmbeddedArc.Arc.sliceParam line 87
  17. lemma OAI.CannonEmbeddedArc.Arc.spliceFun_middle line 94
  18. lemma OAI.CannonEmbeddedArc.Arc.spliceFun_outside line 105
  19. lemma OAI.CannonEmbeddedArc.Arc.injective_spliceFun line 112
  20. def OAI.CannonEmbeddedArc.Arc.splice line 132
  21. lemma OAI.CannonEmbeddedArc.Arc.splice_range_subset line 138
  22. lemma OAI.CannonEmbeddedArc.Arc.splice_zero line 150
  23. lemma OAI.CannonEmbeddedArc.Arc.splice_one line 156
  24. lemma OAI.CannonEmbeddedArc.Arc.sliceParam_interior line 162
  25. lemma OAI.CannonEmbeddedArc.Arc.spliceFun_same_outside_open line 172
  26. lemma OAI.CannonEmbeddedArc.Arc.splice_preimage line 179
  27. lemma OAI.CannonEmbeddedArc.Arc.ordConnected_sdiff_Ioo line 193
  28. lemma OAI.CannonEmbeddedArc.Arc.splice_ordConnected line 204
  29. lemma OAI.CannonEmbeddedArc.Arc.first_last line 214
  30. lemma OAI.CannonEmbeddedArc.Arc.splice_target_preimage line 223
  31. lemma OAI.CannonEmbeddedArc.Arc.subarc_interior_parameter line 237
  32. def OAI.CannonEmbeddedArc.Arc.Compatible line 250
  33. lemma OAI.CannonEmbeddedArc.Arc.Compatible.symm line 254
  34. lemma OAI.CannonEmbeddedArc.Arc.Compatible.subarc_avoids line 260
  35. lemma OAI.CannonEmbeddedArc.Arc.Compatible.subarc_not_both line 269
  36. theorem OAI.CannonEmbeddedArc.Arc.repair_one line 276
  37. theorem OAI.CannonEmbeddedArc.Arc.repair_finite line 343
  38. lemma OAI.CannonEmbeddedArc.Arc.intersection_preconnected line 392
  39. theorem OAI.CannonEmbeddedArc.Arc.repair_finite_bounded line 400
  40. lemma OAI.CannonEmbeddedArc.Arc.separated_of_near line 424
  41. lemma OAI.CannonEmbeddedArc.Arc.meets_at_most_one line 437
  42. def OAI.CannonEmbeddedArc.Arc.mappedSegment line 451
  43. lemma OAI.CannonEmbeddedArc.Arc.mappedSegment_zero line 456
  44. lemma OAI.CannonEmbeddedArc.Arc.mappedSegment_one line 459
  45. lemma OAI.CannonEmbeddedArc.Arc.mappedSegment_range line 463