Compactness of the carrier of a polygonal arc
ProvedPolygonalArcCarrierCompactcrossing-consequencesgeometrypolygonal
For every polygonal arc γ, its carrier—the finite union of the closed line segments joining consecutive vertices—is a compact subset of the Euclidean plane. This compactness is the structural finiteness input used to cut away a neighborhood of an endpoint while retaining a compact arc tail.
Preamble
import Definitions.Def_PolygonalArc open Classical noncomputable section
Formal statement
lemma PolygonalArcCarrierCompact (γ : PolygonalArc) : IsCompact γ.carrier := by sorry
Source