English
Let S be a simplicial set. For indices i in Fin(n+2) and j in Fin(n+1) with i ≤ cast Succ(j), and for x in S_{⟦n+1⟧}, the face map δ at castSucc(i) composed with the degeneracy σ at j.succ agrees with the degeneracy σ at j composed with the face δ at i: δ_{castSucc(i)}(σ_j.succ(x)) = σ_j(δ_i(x)).
Русский
Пусть S — симплициальное множество. Пусть i ∈ Fin(n+2) и j ∈ Fin(n+1) такие, что i ≤ castSucc(j), и возьмём x в S_{⟦n+1⟧}. Тогда композиция: δ_{castSucc(i)} после σ_j.succ равна σ_j после δ_i: δ_{castSucc(i)}(σ_j.succ(x)) = σ_j(δ_i(x)).
LaTeX
$$$ \\delta_{\\mathrm{castSucc}(i)}\\big(\\sigma_j^{\\mathrm{succ}}(x)\\big) = \\sigma_j\\big(\\delta_i(x)\\big) \quad\\text{for } i \\in \\mathrm{Fin}(n+2),\\ j \\in \\mathrm{Fin}(n+1),\\ i \\le \\mathrm{castSucc}(j).$$
Lean4
theorem δ_comp_σ_of_le_apply {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) (x : S _⦋n + 1⦌) :
S.δ (Fin.castSucc i) (S.σ j.succ x) = S.σ j (S.δ i x) :=
congr_fun (S.δ_comp_σ_of_le H) x
