Arc-crossing segment chain assembly
ProvedArcCrossingSegmentChainAssemblyA list of vertices with a polygonal path piece between each consecutive pair can be assembled into a finite ordered list of polygonal paths with matching endpoints and a common carrier containment set.
Preamble
import Definitions.Def_PolygonalPath open Classical noncomputable section
Formal statement
lemma ArcCrossingSegmentChainAssembly
(V : List (EuclideanSpace ℝ (Fin 2)))
(source target : EuclideanSpace ℝ (Fin 2))
(S : Set (EuclideanSpace ℝ (Fin 2))) :
V.head? = some source →
V.getLast? = some target →
1 < V.length →
(∀ (i : ℕ) (hi : i + 1 < V.length),
∃ η : PolygonalPath,
η.source = V[i] ∧
η.target = V[i + 1] ∧
η.carrier ⊆ S) →
∃ (pieces : List PolygonalPath) (first last : PolygonalPath),
pieces.head? = some first ∧
pieces.getLast? = some last ∧
first.source = source ∧
last.target = target ∧
(∀ η : PolygonalPath, η ∈ pieces → η.carrier ⊆ S) ∧
(∀ (i : ℕ) (hi : i + 1 < pieces.length),
(pieces[i]).target = (pieces[i + 1]).source) := by sorrySource