Terminal endpoint segment length of a polygonal arc

Definition

PolygonalArcTerminalEndpointSegmentLength

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

crossing-consequencespolygonal-geometry

The Euclidean length of the final edge of a polygonal arc, measured from its terminal endpoint to its preceding vertex.

Definition code

import Mathlib.Tactic
import Definitions.Def_PolygonalArc

open Classical
noncomputable section

-- [TABLET NODE: PolygonalArcTerminalEndpointSegmentLength]
-- Source: https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcTerminalEndpointSegmentLength.lean#L1-L11
def PolygonalArcTerminalEndpointSegmentLength (γ : PolygonalArc) : ℝ :=
  let hprev : γ.vertices.length - 2 < γ.vertices.length := by
    have hlen := γ.length_ge_two
    omega
  dist γ.target (γ.vertices[γ.vertices.length - 2]'hprev)

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcTerminalEndpointSegmentLength.lean

View graph