σ_comp_σ_apply — Mathlib

English

The degeneracy maps satisfy a braid-like identity: for i ≤ j, σ_i.castSucc (σ_j x) = σ_j.succ (σ_i x).

Русский

Размножающие отображения удовлетворяют браидоподобному тождеству: если i ≤ j, тогда σ_i.castSucc(σ_j x) = σ_{j.succ}(σ_i x).

LaTeX

$$$ \\sigma_i^{\\mathrm{castSucc}}(\\sigma_j x) = \\sigma_{j}\\!\\text{-succ}(\\sigma_i x) \\quad\\text{for } i \\le j$$$

Lean4

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

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