δ_comp_σ_of_gt — Mathlib

English

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

Русский

Если j.castSucc < i, то δ_{i.castSucc} ∘ σ_{j.castSucc} = σ_j ∘ δ_i.

LaTeX

$$$\delta_{i.castSucc} \circ \sigma_{j.castSucc} = \sigma_j \circ \delta_i \quad (j.castSucc < i)$$$

Lean4

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

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