Interior parameters of polygonal routes

An interior parameter of any listed segment lies strictly between the two original route ends. This separates actual segment interiors from permitted loop closure contacts.

theorem Cslib.Polygonal.Route.not_atEnd_of_mem_Ioo (p : Route) (i : Fin p.segments) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (tag : Bool) : ¬p.AtEnd i t tag

An interior segment parameter is never either original route end.