δ_comp_δ_self — Mathlib

English

Special case of the first simplicial identity: δ_i.castSucc ≫ δ_i = δ_i.succ ≫ δ_i.

Русский

Особый случай первой симпликал-идентичности: δ_i.castSucc ∘ δ_i = δ_i.succ ∘ δ_i.

LaTeX

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

Lean4

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

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