Translating finite polygonal routes

Translation acts on every listed point and every actual segment, preserves the route parameter and its two ends, and leaves outgoing germs unchanged.

def Cslib.Polygonal.Route.translate (p : Route) (z : ℂ) : Route

Translate every point of a finite polygonal route by the same plane vector.

@[simp]

theorem Cslib.Polygonal.Route.eval_translate (p : Route) (z : ℂ) (i : Fin p.segments) (t : ℝ) : (p.translate z).eval i t = z + p.eval i t

Translation commutes with the actual affine segment evaluation.

@[simp]

theorem Cslib.Polygonal.Route.endpoint_translate (p : Route) (z : ℂ) (b : Bool) : (p.translate z).endpoint b = z + p.endpoint b

Translation moves either endpoint by the same plane vector.

@[simp]

theorem Cslib.Polygonal.Route.germ_translate (p : Route) (z : ℂ) (b : Bool) : (p.translate z).germ b = p.germ b

Translation preserves the actual outgoing end vectors, including both loop ends.

theorem Cslib.Polygonal.Route.IsSimple.translate {p : Route} (hp : p.IsSimple) (z : ℂ) : (p.translate z).IsSimple

Translating a simple route preserves simplicity at every real segment parameter.