A polygonal-arc vertex avoids every nonincident segment
ProvedPolygonalArcVertexAvoidsNonincidentSegmentcrossing-consequencesgeometrypolygonal
Let γ be a polygonal arc with vertices p₀, p₁, …, and let [pⱼ,pⱼ₊₁] be one of its listed segments. If the vertex index i is different from both j and j+1, then the vertex pᵢ does not belong to the closed segment [pⱼ,pⱼ₊₁]. The conclusion uses the defining properties of a polygonal arc: its listed vertices are pairwise distinct, and no vertex lies in the relative interior of a nonincident listed segment.
Preamble
import Definitions.Def_PolygonalArc open Classical noncomputable section
Formal statement
lemma PolygonalArcVertexAvoidsNonincidentSegment (γ : PolygonalArc)
{i j : ℕ} (hi : i < γ.vertices.length)
(hj : j + 1 < γ.vertices.length) (hij : i ≠ j) (hijs : i ≠ j + 1) :
γ.vertices[i] ∉ segment ℝ γ.vertices[j] γ.vertices[j + 1] := by sorrySource