Connectedness of a polygonal path carrier
ProvedPolygonalPathCarrierConnectedFor every polygonal path in the Euclidean plane, the path carrier is connected. The carrier consists of the path's endpoints together with the line segments joining consecutive vertices, so this lemma provides the connectedness fact needed when a polygonal path meets an open cover.
Preamble
import Definitions.Def_PolygonalPath open Classical noncomputable section -- [TABLET NODE: PolygonalPathCarrierConnected]
Formal statement
lemma PolygonalPathCarrierConnected (γ : PolygonalPath) : IsConnected γ.carrier := by sorry
Source