δ_comp_δ''_apply — Mathlib

English

A similar relation for δ_i with δ_j where indices satisfy castLT-based ordering; describes how δ_i castLT interacts with δ_j.

Русский

Аналогичное отношение δ_i с δ_j, когда индексы удовлетворяют порядку по castLT; описывает взаимодействие δ_i castLT с δ_j.

LaTeX

$$$ S.\delta_i^{\mathrm{castLT}} \circ S.\delta_j = S.\delta_j \circ S.\delta_i \quad (\text{with appropriate ordering}) $$$

Lean4

theorem δ_comp_δ''_apply {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) (x : S _⦋n + 2⦌) :
    S.δ (i.castLT (Nat.lt_of_le_of_lt (Fin.le_iff_val_le_val.mp H) j.is_lt)) (S.δ j.succ x) = S.δ j (S.δ i x) :=
  congr_fun (S.δ_comp_δ'' H) x

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