δ_comp_σ_of_le — Mathlib

English

If i ≤ castSucc j, then δ_{castSucc i} ≫ σ_j.succ = σ_j ≫ δ_i.

Русский

При i ≤ castSucc j выполняется δ_{castSucc i} ∘ σ_{j.succ} = σ_j ∘ δ_i.

LaTeX

$$$\delta_{\mathrm{castSucc}\,i} \circ \sigma_{j}^{\mathrm{succ}} = \sigma_j \circ \delta_i \quad (i\leq\mathrm{castSucc}(j))$$$

Lean4

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

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