smash_natAdd — Mathlib

English

For p, q and i, smashing p with q respects natural-number length addition: smash p q h (i.natAdd p.length).castSucc = q i.castSucc.

Русский

Слияние p и q с учётом натурального дополнения длины: smash p q h (i.natAdd p.length).castSucc = q i.castSucc.

LaTeX

$$$ smash\ p\ q\ h (i.natAdd p.length).castSucc = q i.castSucc $$$

Lean4

theorem smash_natAdd {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) :
    smash p q h (i.natAdd p.length).castSucc = q i.castSucc :=
  by
  dsimp only [smash, Fin.castSucc_natAdd]
  apply Fin.addCases_right

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