δ₂_zero_comp_σ₂_one — Mathlib

English

In the truncated simplex setting, the relation between δ₂ at 0 and σ₂ at 1 and between σ₂ at 0 and δ₂ at 0 holds: δ₂(0) ∘ σ₂(1) = σ₂(0) ∘ δ₂(0).

Русский

В усечённой симплициальной категории выполняется: δ₂(0) ∘ σ₂(1) = σ₂(0) ∘ δ₂(0).

LaTeX

$$$$ \delta_{2}(0) \circ \sigma_{2}(1) = \sigma_{2}(0) \circ \delta_{2}(0) $$$$

Lean4

@[reassoc]
theorem δ₂_zero_comp_σ₂_one : δ₂ (0 : Fin 3) ≫ σ₂ 1 = σ₂ 0 ≫ δ₂ 0 :=
  SimplexCategory.δ_comp_σ_of_le (i := 0) (j := 0) (Fin.zero_le _)

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