Prove2Me

Finite polygonal path chain concatenation

Proved
PolygonalPathFiniteChainConcat

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

A finite list of polygonal paths with matching consecutive endpoints and carriers in a common set can be concatenated into one polygonal path joining the first source to the last target and remaining in that set.

Preamble
import Definitions.Def_PolygonalPath

open Classical
noncomputable section
Formal statement
lemma PolygonalPathFiniteChainConcat
    (S : Set (EuclideanSpace ℝ (Fin 2))) :
    ∀ (pieces : List PolygonalPath) (first last : PolygonalPath),
      pieces.head? = some first →
        pieces.getLast? = some last →
          (∀ η : PolygonalPath, η ∈ pieces → η.carrier ⊆ S) →
            (∀ (i : ℕ) (hi : i + 1 < pieces.length),
              (pieces[i]).target = (pieces[i + 1]).source) →
              ∃ ζ : PolygonalPath,
                ζ.source = first.source ∧
                  ζ.target = last.target ∧
                    ζ.carrier ⊆ S := by sorry
Source
https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalPathFiniteChainConcat.lean#L1-L63

View graph