δ_comp_σ_succ — Mathlib

English

The second part of the third simplicial identity: δ i.succ ≫ σ i = 𝟙 holds in Δ^n, i.e., the appropriate composition equals the identity.

Русский

Вторая часть третьей симпликальной идентичности: δ_i.succ ∘ σ_i = id в Δ^n.

LaTeX

$$δ i.succ ≫ σ i = id_{Δ^n}$$

Lean4

/-- The second part of the third simplicial identity -/
@[reassoc]
theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : δ i.succ ≫ σ i = 𝟙 ⦋n⦌ :=
  by
  ext j
  rcases i with ⟨i, _⟩
  rcases j with ⟨j, _⟩
  dsimp [δ, σ, Fin.succAbove, Fin.predAbove]
  split_ifs <;> simp <;> simp at * <;> omega

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