snoc_cast_castSucc — Mathlib

English

For p, a, h and i ∈ Fin(p.length+1), the value at index i.castSucc of p.snoc a h equals the value at index i of p: (p.snoc a h).toFun (i.castSucc) = p.toFun i.

Русский

Для p, a, h и i ∈ Fin(p.length+1) значение на позиции i.castSucc в p.snoc a h равно значению на позиции i в p: (p.snoc a h).toFun (i.castSucc) = p.toFun i.

LaTeX

$$$ (p.\text{snoc } a\ h).toFun (i.castSucc) = p.toFun i $$$

Lean4

theorem snoc_cast_castSucc (s : RelSeries r) (a : α) (h : s.last ~[r] a) (i : Fin (s.length + 1)) :
    (s.snoc a h) (.cast (by simp) (.castSucc i)) = s i :=
  append_apply_left s (singleton r a) h i

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