smash_succ_castAdd — Mathlib

English

For p, q and i, smashing with q at index i.castAdd q.length and taking the succ index gives p i.succ: p.smash q h (i.castAdd q.length).succ = p i.succ.

Русский

При слитии p и q на индексе i.castAdd q.length и взятии successor получаем p i.succ.

LaTeX

$$$ p.smash q h (i.castAdd q.length).succ = p i.succ $$$

Lean4

theorem smash_succ_castAdd {p q : RelSeries r} (h : p.last = q.head) (i : Fin p.length) :
    p.smash q h (i.castAdd q.length).succ = p i.succ :=
  smash_castLE h i.succ

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