Arc-crossing segment parameter gap piece
ProvedArcCrossingSegmentParameterGapPieceA parameter interval lying strictly between consecutive intersection parameters on a polygonal path segment can be replaced by a polygonal path with the same endpoints that avoids both the forbidden set and the polygonal arc.
Preamble
import Definitions.Def_PolygonalArc import Definitions.Def_PolygonalPath open Classical noncomputable section
Formal statement
lemma ArcCrossingSegmentParameterGapPiece
(K : Set (EuclideanSpace ℝ (Fin 2))) (γ : PolygonalArc) (α : PolygonalPath)
(i : ℕ) (hi : i + 1 < α.vertices.length) (left right s t : ℝ) :
α.carrier ⊆ Kᶜ →
left < s →
s ≤ t →
t < right →
0 < left →
right < 1 →
(∀ u : ℝ, 0 < u → u < 1 →
(AffineMap.lineMap α.vertices[i] α.vertices[i + 1]) u ∈ γ.carrier →
¬ (left < u ∧ u < right)) →
∃ η : PolygonalPath,
η.source =
(AffineMap.lineMap α.vertices[i] α.vertices[i + 1]) s ∧
η.target =
(AffineMap.lineMap α.vertices[i] α.vertices[i + 1]) t ∧
η.carrier ⊆ (K ∪ γ.carrier)ᶜ := by sorrySource