snoc_castSucc — Mathlib

English

For s, a, connect and i ∈ Fin(s.length+1), the value at i.castSucc in (s.snoc a connect) equals the value at i in s: (s.snoc a connect).toFun i.castSucc = s.toFun i.

Русский

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

LaTeX

$$$ (s.\text{snoc } a\ connect).toFun i.castSucc = s.toFun i $$$

Lean4

@[simp]
theorem snoc_castSucc (s : RelSeries r) (a : α) (connect : s.last ~[r] a) (i : Fin (s.length + 1)) :
    snoc s a connect (Fin.castSucc i) = s i :=
  Fin.append_left _ _ i

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