PolygonalArcCollarMiddleForbiddenMarginsExists
ProvedPolygonalArcCollarMiddleForbiddenMarginsExistscrossing-consequencesgeometrypolygonal
For every polygonal arc, collar-control radii, and middle-segment data, there exists a family of positive forbidden margins separating each middle segment from nonadjacent edges, nonincident control disks, and nonadjacent middle cores.
Preamble
import Definitions.Def_PolygonalArcCollarMiddleForbiddenMargins import Mathlib.Analysis.Normed.Module.Convex open Classical noncomputable section
Formal statement
lemma PolygonalArcCollarMiddleForbiddenMarginsExists (γ : PolygonalArc) {η : ℝ}
(controlRadii : PolygonalArcCollarControlRadii γ η)
(middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii) :
Nonempty (PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments) := by sorrySource