σ_comp_σ — Mathlib

English

The fifth simplicial identity: σ_j ≫ σ_{i.castSucc} = σ_i ≫ σ_{j.succ} under i ≤ j.

Русский

Пятое симпликальное тождество: σ_j ∘ σ_{i.castSucc} = σ_i ∘ σ_{j.succ} при i ≤ j.

LaTeX

$$$X.\sigma_j \circ X.\sigma_{i.castSucc} = X.\sigma_i \circ X.\sigma_{j.succ}$$$

Lean4

/-- The fifth simplicial identity -/
@[reassoc]
theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) : X.σ j ≫ X.σ (Fin.castSucc i) = X.σ i ≫ X.σ j.succ :=
  by
  dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.σ_comp_σ H]

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