PL segment models for polygonal arcs

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.BrokenLineData.exists_PL_segment_model {U : Set Plane} (B : BrokenLineData U) : ∃ (S : PlaneComplex) (F : Plane → Plane), S.support = segment ℝ (planePoint 0 0) (planePoint (↑B.resolvedWalk.length) 0) ∧ IsPLOn S F ∧ (∀ s ∈ S.simplexes, s.card ≤ 2) ∧ Set.InjOn F S.support ∧ F '' S.support = B.resolvedCarrier ∧ F (planePoint 0 0) = B.start ∧ F (planePoint (↑B.resolvedWalk.length) 0) = B.finish

A polygonal arc extracted from a broken line is the endpoint-preserving PL image of a straight segment.