δ_comp_σ_of_gt_apply — Mathlib

English

For i > castSucc(j), the δ_i map composed with σ_{castSucc(j)} equals σ_j composed with δ_i: δ_i(σ_castSucc(j)(x)) = σ_j(δ_i(x)).

Русский

Если i > castSucc(j), то δ_i(σ_castSucc(j)(x)) = σ_j(δ_i(x)).

LaTeX

$$$ \\delta_{i}(\\sigma_{\\mathrm{castSucc}(j)}(x)) = \\sigma_j(\\delta_i(x)) \\quad\\text{when } \\mathrm{castSucc}(j) < i$$$

Lean4

theorem δ_comp_σ_of_gt_apply {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) (x : S _⦋n + 1⦌) :
    S.δ i.succ (S.σ (Fin.castSucc j) x) = S.σ j (S.δ i x) :=
  congr_fun (S.δ_comp_σ_of_gt H) x

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