δ_comp_δ'' — Mathlib

English

A generic δ-δ'' identity in the third simplicial identity: δ_j.succ ∘ δ_i.castLT = δ_i ∘ δ_j.

Русский

Общее тождество δ-δ'' в третьей симпликал-идентичности: δ_{j.succ} ∘ δ_{i.castLT} = δ_i ∘ δ_j.

LaTeX

$$$X.\delta_{j.succ} \circ X.\delta_{i.castLT} = X.\delta_i \circ X.\delta_j$$$

Lean4

@[reassoc]
theorem δ_comp_δ'' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) :
    X.δ j.succ ≫ X.δ (i.castLT (Nat.lt_of_le_of_lt (Fin.le_iff_val_le_val.mp H) j.is_lt)) = X.δ i ≫ X.δ j :=
  by
  dsimp [δ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]

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