Straight segment as a polygonal path

Proved

PolygonalPathSegment

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

geometrypolygonal-paths

For any two points $p$ and $q$ in the Euclidean plane, the straight segment from $p$ to $q$ is the carrier of a polygonal path with source $p$ and target $q$ .

Preamble

import Definitions.Def_PolygonalPath

open Classical
noncomputable section

Formal statement

lemma PolygonalPathSegment
    (p q : EuclideanSpace ℝ (Fin 2)) :
    ∃ γ : PolygonalPath,
      γ.source = p ∧
        γ.target = q ∧
          γ.carrier = segment ℝ p q := by sorry

Source

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

View graph