Arc-crossing cut window parameters
ProvedArcCrossingCutWindowParametersIf a point in the interior of a polygonal path segment has two prescribed points approaching it from the two sides, then those points are represented by affine parameters strictly before and after the parameter of the intersection point.
Preamble
import Definitions.Def_PolygonalPath open Classical noncomputable section
Formal statement
lemma ArcCrossingCutWindowParameters
(α : PolygonalPath) (i : ℕ) (hi : i + 1 < α.vertices.length)
(x before after : EuclideanSpace ℝ (Fin 2)) (p : ℝ) :
0 < p →
p < 1 →
AffineMap.lineMap α.vertices[i] α.vertices[i + 1] p = x →
before ∈ openSegment ℝ α.vertices[i] x →
after ∈ openSegment ℝ x α.vertices[i + 1] →
∃ b a : ℝ,
0 < b ∧ b < p ∧ p < a ∧ a < 1 ∧
AffineMap.lineMap α.vertices[i] α.vertices[i + 1] b = before ∧
AffineMap.lineMap α.vertices[i] α.vertices[i + 1] a = after := by sorrySource