Arc-crossing segment boundary gap piece
ProvedArcCrossingSegmentBoundaryGapPieceA closed parameter interval in a polygonal path segment containing no intersection with the polygonal arc, including possible endpoints, admits a safe polygonal replacement joining its affine endpoints.
Preamble
import Definitions.Def_PolygonalArc import Definitions.Def_PolygonalPath open Classical noncomputable section
Formal statement
lemma ArcCrossingSegmentBoundaryGapPiece
(K : Set (EuclideanSpace ℝ (Fin 2))) (γ : PolygonalArc) (α : PolygonalPath)
(i : ℕ) (hi : i + 1 < α.vertices.length) (s t : ℝ) :
α.carrier ⊆ Kᶜ →
0 ≤ s →
s ≤ t →
t ≤ 1 →
α.vertices[i] ∉ γ.carrier →
α.vertices[i + 1] ∉ γ.carrier →
(∀ u : ℝ, 0 < u → u < 1 →
(AffineMap.lineMap α.vertices[i] α.vertices[i + 1]) u ∈ γ.carrier →
¬ (s ≤ u ∧ u ≤ t)) →
∃ η : PolygonalPath,
η.source =
(AffineMap.lineMap α.vertices[i] α.vertices[i + 1]) s ∧
η.target =
(AffineMap.lineMap α.vertices[i] α.vertices[i + 1]) t ∧
η.carrier ⊆ (K ∪ γ.carrier)ᶜ := by sorrySource