δ₂_two_comp_σ₂_one — Mathlib

English

In the truncated simplex category, the composition δ₂(2) ∘ σ₂(1) equals the identity morphism.

Русский

В усечённой симплициальной категории композиция δ₂(2) ∘ σ₂(1) равна тождественному морфизму.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem δ₂_two_comp_σ₂_one : δ₂ (2 : Fin 3) ≫ σ₂ 1 = 𝟙 _ :=
  SimplexCategory.δ_comp_σ_succ' (by decide)

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