Constant polygonal path

Proved

PolygonalPathConstant

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

geometrypolygonal-paths

For every point $p$ in the Euclidean plane, there is a polygonal path whose source and target are both $p$ and whose carrier is exactly the singleton $\{p\}$ .

Preamble

import Definitions.Def_PolygonalPath

open Classical
noncomputable section

Formal statement

lemma PolygonalPathConstant (p : EuclideanSpace ℝ (Fin 2)) :
    ∃ γ : PolygonalPath,
      γ.source = p ∧
        γ.target = p ∧
          γ.carrier = ({p} : Set (EuclideanSpace ℝ (Fin 2))) := by sorry

Source

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

View graph