Open polygonal-arc segments lie in the relative interior
ProvedPolygonalArcOpenSegmentSubsetRelativeInteriorcrossing-consequencesgeometrypolygonal
Let γ be a polygonal arc and let j index one of its consecutive edges. Every point of the open segment between γ.vertices[j] and γ.vertices[j+1] belongs to γ's relative interior. The endpoint exclusions follow from the arc's simple-vertex and nonincident-interior conditions, so an open edge contributes no endpoint to the relative boundary.
Preamble
import Definitions.Def_PolygonalArc open Classical noncomputable section
Formal statement
lemma PolygonalArcOpenSegmentSubsetRelativeInterior (γ : PolygonalArc) (j : ℕ)
(hj : j + 1 < γ.vertices.length) :
openSegment ℝ γ.vertices[j] γ.vertices[j + 1] ⊆ γ.relativeInterior := by sorrySource