English
When i > j in the adjusted indexing, δ_i(σ_j x) equals a shifted degeneracy σ_{j.castLT(…) } applied to δ_{i.pred(…)} x, formalizing the index reparametrization in the commutation of δ and σ.
Русский
При i > j в исправленной системе индексации δ_i(σ_j x) равняется сдвинутому σ_{j.castLT(…)} применённому к δ_{i.pred(…)} x, формализуя переназначение индексов в لكمтации δ и σ.
LaTeX
$$$ \\delta_i(\\sigma_j(x)) = \\sigma_{j\\text{.castLT}(\\dots)}(\\delta_{i\\text{.pred}(\\dots)}(x)) \\quad\\text{when } j < i$$$
Lean4
theorem δ_comp_σ_of_gt'_apply {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) (x : S _⦋n + 1⦌) :
S.δ i (S.σ j x) =
S.σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le)))
(S.δ (i.pred fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) x) :=
congr_fun (S.δ_comp_σ_of_gt' H) x
