δ_comp_δ — Mathlib

English

For all n and i ≤ j, δ_i ≫ δ_{j+1} = δ_j ≫ δ_i.castSucc.

Русский

Для всех n и i ≤ j выполняется δ_i ∘ δ_{j+1} = δ_j ∘ δ_i^{castSucc}.

LaTeX

$$$$ δ_i \\circ δ_{j+1} = δ_j \\circ δ_i^{\\mathrm{castSucc}} \\quad \\text{for } i \\le j $$$$

Lean4

@[reassoc]
theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) : δ i ≫ δ j.succ = δ j ≫ δ i.castSucc :=
  by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.δ_comp_δ H

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