δ_comp_δ_self' — Mathlib

English

A variant stating δ_i ≫ δ_j equals δ_j.succ ≫ δ_i under a relabeled index.

Русский

Вариант тождества δ-δ_self' с переименованием индексов: δ_i ≫ δ_j = δ_j.succ ≫ δ_i.

LaTeX

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

Lean4

@[reassoc]
theorem δ_comp_δ_self' {n} {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = Fin.castSucc i) :
    X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i := by
  subst H
  rw [δ_comp_δ_self]

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