δ_comp_σ_of_gt — Mathlib

English

Let n be a natural number, i in Fin(n+2) and j in Fin(n+1) with j.castSucc < i. Then δ i.succ ∘ σ j.castSucc = σ j ∘ δ i.

Русский

Пусть n — натуральное число, i ∈ Fin(n+2) и j ∈ Fin(n+1) удовлетворяют j.castSucc < i. Тогда δ i.succ ∘ σ j.castSucc = σ j ∘ δ i.

LaTeX

$$$\delta_{i+1} \circ \sigma_{j}^{\mathrm{castSucc}} = \sigma_j \circ \delta_i \quad\text{при } j^{\mathrm{castSucc}} < i$$$

Lean4

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

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