append_apply_right — Mathlib

English

Similarly, the i-th element on the right part of p.concat(q) equals the i-th element of q for i in the right segment.

Русский

Аналогично, i-й элемент правой части p ∘ q равен i-му элементу q для i в правой части.

LaTeX

$$$ (p \\append q \\;\\text{connect}).toFun (i) = q(i) \\quad\\text{for } i < q.length + 1 $$$

Lean4

theorem append_apply_right (p q : RelSeries r) (connect : p.last ~[r] q.head) (i : Fin (q.length + 1)) :
    p.append q connect ((i.natAdd (p.length + 1)).cast (by dsimp; cutsat) : Fin ((p.append q connect).length + 1)) =
      q i :=
  Fin.append_right _ _ _

Похожие утверждения