Polygonal path original segment gap
ProvedPolygonalPathOriginalSegmentGapA subsegment of an original polygonal path segment that is disjoint from a forbidden set can be replaced by a polygonal path whose carrier avoids the forbidden set and a prescribed set avoided by the original path.
Preamble
import Definitions.Def_PolygonalPath open Classical noncomputable section
Formal statement
lemma PolygonalPathOriginalSegmentGap
(K F : Set (EuclideanSpace ℝ (Fin 2))) (α : PolygonalPath)
(i : ℕ) (hi : i + 1 < α.vertices.length)
(p q : EuclideanSpace ℝ (Fin 2)) :
α.carrier ⊆ Kᶜ →
segment ℝ p q ⊆ segment ℝ α.vertices[i] α.vertices[i + 1] →
Disjoint (segment ℝ p q) F →
∃ η : PolygonalPath,
η.source = p ∧
η.target = q ∧
η.carrier ⊆ (K ∪ F)ᶜ := by sorrySource