δ_comp_σ_self' — Mathlib

English

A variant of the first simplicial identity stating δ_j ≫ δ_i = δ_i ≫ δ_i.succ when j = i.castSucc.

Русский

Вариант первой симпликальной идентичности: δ_j ≫ δ_i = δ_i ≫ δ_i.succ при j = i.castSucc.

LaTeX

$$δ_j ≫ δ_i = δ_i ≫ δ_i.succ при j = i.castSucc$$

Lean4

@[reassoc]
theorem δ_comp_σ_self' {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) : δ j ≫ σ i = 𝟙 ⦋n⦌ :=
  by
  subst H
  rw [δ_comp_σ_self]

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