castSucc_castAdd — Mathlib

English

Casting after adding m to i and then applying castSucc equals casting after adding m+1 to i.

Русский

После сложения m к i и применения castSucc результат равенCastAdd(m+1) к i.

LaTeX

$$$$ \\forall {n,m} \\ (i \\in \\mathrm{Fin}(n)): \\operatorname{castSucc}(\\operatorname{castAdd} m \\ i) = \\operatorname{castAdd}(m+1) \\ i. $$$$

Lean4

theorem castSucc_castAdd (i : Fin n) : castSucc (castAdd m i) = castAdd (m + 1) i :=
  rfl

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