δ_comp_δ' — Mathlib

English

A general form of the first cosimplicial identity with a refined indexing: δ_i.castLT and δ_j.succ relate by δ_j.pred and cast results as per the lemma.

Русский

Обобщённая форма первого косимпликсного тождества со скорректированными индексами: δ_i.castLT и δ_j.succ связаны через δ_j.pred и соответствующие преобразования cast.

LaTeX

$$$\delta\_{i}^{\mathrm{castLT}} \circ \delta\_{j}^{\mathrm{succ}} = \delta\_{j}^{\,\mathrm{pred}} \circ \delta\_{i}^{\mathrm{castSucc}}$ (в соответствующих условиях)$$

Lean4

@[reassoc]
theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) :
    X.δ i ≫ X.δ j = X.δ (j.pred fun (hj : j = 0) => by simp only [hj, Fin.not_lt_zero] at H) ≫ X.δ (Fin.castSucc i) :=
  by
  dsimp [δ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_δ' H]

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