δ_comp_σ_succ — Mathlib

English

The second part of the third simplicial identity: δ_i.succ ≫ σ_j = σ_j ≫ δ_i for suitable indices.

Русский

Вторая часть третьего симпликального тождества: δ_i.succ ∘ σ_j = σ_j ∘ δ_i для совместимых индексов.

LaTeX

$$$X.\delta_{i.succ} \circ X.\sigma_j = X.\sigma_j \circ X.\delta_i$$$

Lean4

/-- The second part of the third simplicial identity -/
@[reassoc]
theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : X.σ i ≫ X.δ i.succ = 𝟙 _ :=
  by
  dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_succ, op_id, X.map_id]

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