δ_comp_σ_succ'_apply — Mathlib

English

If j = i.succ, then δ_j(σ_i(x)) = x for x ∈ S_{⟦n⟧}. This expresses a boundary-degeneracy cancellation at a shifted index.

Русский

Если j = i.succ, то δ_j(σ_i(x)) = x для x ∈ S_{⟦n⟧}. Это выражает отмену границы и разряда по смещённому индексу.

LaTeX

$$$ \\delta_{j}(\\sigma_{i}(x)) = x \\quad\\text{when } j = i^{\\mathrm{succ}}$$$

Lean4

theorem δ_comp_σ_succ'_apply {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) (x : S _⦋n⦌) :
    S.δ j (S.σ i x) = x :=
  congr_fun (S.δ_comp_σ_succ' H) x

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