Single-segment polygonal routes

The one-segment constructor and simplicity criterion connect finite route data to Mathlib's actual real affine segment. In particular a one-segment loop is not simple.

def Cslib.Polygonal.Route.line (a b : ℂ) : Route

One actual real planar segment, including its two distinct parameter ends.

@[simp]

theorem Cslib.Polygonal.Route.start_line (a b : ℂ) : (line a b).start = a

The first end of a single-segment route.

@[simp]

theorem Cslib.Polygonal.Route.finish_line (a b : ℂ) : (line a b).finish = b

The last end of a single-segment route.

theorem Cslib.Polygonal.Route.eval_line (a b : ℂ) (i : Fin (line a b).segments) (t : ℝ) : (line a b).eval i t = (AffineMap.lineMap a b) t

Evaluating the single-segment route is Mathlib's full real affine interpolation.

theorem Cslib.Polygonal.Route.isSimple_line {a b : ℂ} (hab : a ≠ b) : (line a b).IsSimple

A segment joining distinct points is a simple polygonal route.

theorem Cslib.Polygonal.Route.isSimple_line_iff (a b : ℂ) : (line a b).IsSimple ↔ a ≠ b

Nondegeneracy is necessary as well as sufficient, even if a route is allowed to close.