δ_comp_σ_of_le — Mathlib

English

For all n, i, j with i ≤ j.cast Succ, δ i.castSucc ≫ σ j.succ = σ j ≫ δ i.

Русский

Для всех n, i, j с i ≤ j.castSucc выполняется δ i.castSucc ∘ σ j.succ = σ j ∘ δ i.

LaTeX

$$$$ δ_{i}^{\\mathrm{castSucc}} \\circ σ_{j}^{\\mathrm{succ}} = σ_j \\circ δ_i $$$$

Lean4

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

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