Initial endpoint segment length of a polygonal arc
DefinitionPolygonalArcInitialEndpointSegmentLengthcrossing-consequencespolygonal-geometry
The Euclidean length of the first edge of a polygonal arc, measured from its initial endpoint to its first subsequent vertex.
Definition code
import Definitions.Def_PolygonalArc open Classical noncomputable section -- [TABLET NODE: PolygonalArcInitialEndpointSegmentLength] -- Source: https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcInitialEndpointSegmentLength.lean#L1-L10 def PolygonalArcInitialEndpointSegmentLength (γ : PolygonalArc) : ℝ := let hfirst : 1 < γ.vertices.length := Nat.lt_of_succ_le γ.length_ge_two dist γ.source (γ.vertices[1]'hfirst)
Source