Single-vertex polygonal screening

Proved

SingleVertexPolygonalScreening

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry

Given a point a outside a finite polygonal set K and a nonempty open set W, there is a point x in W outside K such that the segment from a to x avoids every listed point and has neither a nontrivial common subsegment nor a parallel interior crossing with any listed segment of K.

Preamble

import Definitions.Def_FinitePolygonalSet
open Classical
noncomputable section

Formal statement

lemma SingleVertexPolygonalScreening
    (K : FinitePolygonalSet) (a : EuclideanSpace ℝ (Fin 2))
    (W : Set (EuclideanSpace ℝ (Fin 2)))
    (ha : a ∉ K.carrier) (hWopen : IsOpen W) (hWnonempty : W.Nonempty) :
    ∃ x ∈ W, x ∉ K.carrier ∧
      (∀ p : EuclideanSpace ℝ (Fin 2), p ∈ K.points → p ∉ segment ℝ a x) ∧
      (∀ s : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2), s ∈ K.segments →
          ¬ ∃ p q : EuclideanSpace ℝ (Fin 2), p ≠ q ∧
            segment ℝ p q ⊆ segment ℝ a x ∩ segment ℝ s.1 s.2) ∧
      (∀ (s : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)), s ∈ K.segments →
        ∀ p : EuclideanSpace ℝ (Fin 2),
          p ∈ openSegment ℝ a x → p ∈ openSegment ℝ s.1 s.2 →
            ¬ ∃ c : ℝ, s.2 - s.1 = c • (x - a)) := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/SingleVertexPolygonalScreening.lean#L1-L161

View graph