δ_comp_δ — Mathlib

English

For a cosimplicial object X, the relation δ_i ≫ δ_{j+1} = δ_j ≫ δ_{i+1} holds when i ≤ j.

Русский

Для косимпликсного объекта X верно δ_i ∘ δ_{j+1} = δ_j ∘ δ_{i+1}, если i ≤ j.

LaTeX

$$$\delta_i \circ \delta_{j+1} = \delta_j \circ \delta_{i+1} \quad (i \le j)$$$

Lean4

/-- The generic case of the first cosimplicial identity -/
@[reassoc]
theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) : X.δ i ≫ X.δ j.succ = X.δ j ≫ X.δ (Fin.castSucc i) :=
  by
  dsimp [δ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_δ H]

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