δ_comp_δ'_apply — Mathlib

English

More refined relations between δ maps δ_i and δ_j when indices satisfy certain orderings; expresses how δ_i and δ_j compose with adjusted indices.

Русский

Более точные соотношения между δ_i и δ_j при заданном порядке индексов; описывает композицию δ с поправками индексов.

LaTeX

$$$\forall S,n,i,j,\; (H:\text{castSucc}(i) < j)\Rightarrow S.\delta_i \circ S.\delta_j = S.\delta_{\mathrm{pred}(j)} \circ S.\delta_i^{\mathrm{castSucc}}$$$

Lean4

theorem δ_comp_δ'_apply {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) (x : S _⦋n + 2⦌) :
    S.δ i (S.δ j x) = S.δ (j.pred fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) (S.δ i.castSucc x) :=
  congr_fun (S.δ_comp_δ' H) x

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