English
For p, q and a connecting edge between p and q, the i-th element on the left part of p.concat(q) equals the i-th element of p for i in the left segment.
Русский
Для p, q и соединяющего ребра между p и q, i-й элемент на левой части p ∘ q равен i-му элементу p для i в левой части.
LaTeX
$$$ (p \\append q \\;\\text{connect}).toFun (i) = p(i) \\quad\\text{for } i < p.length + 1 $$$
Lean4
theorem append_apply_left (p q : RelSeries r) (connect : p.last ~[r] q.head) (i : Fin (p.length + 1)) :
p.append q connect ((i.castAdd (q.length + 1)).cast (by dsimp; cutsat) : Fin ((p.append q connect).length + 1)) =
p i :=
by
delta append
simp only [Function.comp_apply]
convert Fin.append_left _ _ _
