PolygonalArcCollarMiddleSegmentDataExists
ProvedPolygonalArcCollarMiddleSegmentDataExistscrossing-consequencesgeometrypolygonal
For every polygonal arc and collar-control radii, there exists middle-segment data selecting nonempty compact subsegments of all edges with the prescribed parameter and neighborhood properties.
Preamble
import Definitions.Def_PolygonalArcCollarMiddleSegmentData open Classical noncomputable section
Formal statement
lemma PolygonalArcCollarMiddleSegmentDataExists (γ : PolygonalArc) {η : ℝ}
(controlRadii : PolygonalArcCollarControlRadii γ η) :
Nonempty (PolygonalArcCollarMiddleSegmentData γ controlRadii) := by sorrySource