Extending a polygonal path by a segment

Proved

PolygonalPathExtendSegment

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

geometrypolygonal-paths

Let $\gamma$ be a polygonal path in a set $S$ , and let the straight segment from its target to a point $z$ also lie in $S$ . Then one can append that segment to obtain a polygonal path from the original source to $z$ whose carrier remains contained in $S$ .

Preamble

import Definitions.Def_PolygonalPath

open Classical
noncomputable section

Formal statement

lemma PolygonalPathExtendSegment
    (S : Set (EuclideanSpace ℝ (Fin 2))) (γ : PolygonalPath)
    (z : EuclideanSpace ℝ (Fin 2)) :
    γ.carrier ⊆ S →
      segment ℝ γ.target z ⊆ S →
        ∃ η : PolygonalPath,
          η.source = γ.source ∧
            η.target = z ∧
              η.carrier ⊆ S := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalPathExtendSegment.lean#L1-L107

View graph