Singleton polygonal path in general position
ProvedSingletonPathInGeneralPositiongeometry
The theorem constructs a degenerate polygonal path consisting only of a point q outside a finite polygonal set K. Its source, target, and carrier are all q, and the path is in general position with respect to K.
Preamble
import Definitions.Def_PolygonalPathInGeneralPosition open Classical noncomputable section
Formal statement
lemma SingletonPathInGeneralPosition (K : FinitePolygonalSet)
(q : EuclideanSpace ℝ (Fin 2)) (hq : q ∉ K.carrier) :
∃ γ : PolygonalPath,
γ.source = q ∧ γ.target = q ∧
γ.carrier = ({q} : Set (EuclideanSpace ℝ (Fin 2))) ∧
PolygonalPathInGeneralPosition γ K := by sorrySource