δ_comp_δ_self_apply — Mathlib

English

For each i, composing δ_i with δ_i.castSucc equals composing δ_i with δ_i.succ on any element.

Русский

Для каждого i композиция δ_i с δ_i.castSucc равна композиции δ_i с δ_i.succ на любом элементе.

LaTeX

$$$ S.\delta_i \circ S.\delta_i^{\mathrm{castSucc}}(x) = S.\delta_i \circ S.\delta_i^{\mathrm{succ}}(x) $$$

Lean4

theorem δ_comp_δ_self_apply {n} {i : Fin (n + 2)} (x : S _⦋n + 2⦌) : S.δ i (S.δ i.castSucc x) = S.δ i (S.δ i.succ x) :=
  congr_fun S.δ_comp_δ_self x

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