Finite polygonal set realizing a polygonal arc
ProvedPolygonalArcFinitePolygonalSetgeometrypolygonal
Every polygonal arc in the plane is the carrier of a finite polygonal set. In other words, for each polygonal arc Γ there is a finite collection of marked points and nondegenerate line segments whose union, together with the marked points, is exactly Γ.carrier, and whose listed segments record all segment intersections as marked points. This finite representation packages the arc in the data structure used for subsequent perturbation and intersection arguments.
Preamble
import Definitions.Def_FinitePolygonalSet import Definitions.Def_PolygonalArc open Classical noncomputable section
Formal statement
lemma PolygonalArcFinitePolygonalSet (Γ : PolygonalArc) :
∃ K : FinitePolygonalSet, K.carrier = Γ.carrier := by sorrySource