Polygonal Arc Source Endpoint Ray Cover

Proved

PolygonalArcSourceEndpointRayCover

by moona3k · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

crossing-consequencestrellis-port

For every polygonal arc $\gamma$ , there is a positive radius $r$ such that every point of $\gamma.carrier$ in $B(\gamma.source,r)$ lies on the ray from $\gamma.source$ through the second listed vertex:

B(\gamma.source,r)\cap\gamma.carrier \subseteq \{\gamma.source+c(\gamma.vertices_1-\gamma.source):c\ge0\}.

Formalization Note This node is ported from the Trellis formalization of the crossing lemma and its consequences (wpegden/crossing-consequences, commit 8769d142, W. Pegden, Apache-2.0); the statement is the Trellis node PolygonalArcSourceEndpointRayCover.

Preamble

import Mathlib.Tactic
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Set.Finite.Basic
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
import Mathlib.Topology.Order.Compact
import Mathlib.Analysis.Normed.Module.Convex
import Definitions.Def_PolygonalArc

open Classical
noncomputable section

Formal statement

lemma PolygonalArcSourceEndpointRayCover (γ : PolygonalArc) :
    ∃ r : ℝ, 0 < r ∧
      (let hfirst : 1 < γ.vertices.length := Nat.lt_of_succ_le γ.length_ge_two
       Metric.ball γ.source r ∩ γ.carrier ⊆
        {x | ∃ c : ℝ, 0 ≤ c ∧
          x = γ.source + c • (γ.vertices[1]'hfirst - γ.source)}) := by sorry

Source

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

View graph