Finite polygonal set with all arc vertices listed
ProvedPolygonalArcFinitePolygonalSetWithVerticesgeometrypolygonal
For every polygonal arc Γ in the plane, there is a finite polygonal set K whose carrier is exactly the carrier of Γ and whose marked point set contains every vertex of Γ. Thus the arc can be represented by finite polygonal data while retaining all of its vertices as listed points.
Preamble
import Definitions.Def_FinitePolygonalSet import Definitions.Def_PolygonalArc open Classical noncomputable section
Formal statement
lemma PolygonalArcFinitePolygonalSetWithVertices (Γ : PolygonalArc) :
∃ K : FinitePolygonalSet,
K.carrier = Γ.carrier ∧
∀ v : EuclideanSpace ℝ (Fin 2), v ∈ Γ.vertices → v ∈ K.points := by sorrySource