δ_comp_δ — Mathlib

English

In the generic case δ_i ≫ δ_j.succ equals δ_j ≫ δ_i.castSucc whenever i ≤ j, reflecting the first simplicial identity in the δ-δ square.

Русский

В обобщённом случае δ_i ∘ δ_j^∘ равняется δ_j ∘ δ_i^cast, если i ≤ j, что выражает первую симпликальную идентичность в квадрате δ-δ.

LaTeX

$$$δ_i \circ δ_j^{\mathrm{succ}} = δ_j \circ δ_i^{\mathrm{castSucc}} \quad \text{при } i \le j$$$

Lean4

/-- The generic case of the first simplicial identity -/
theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) : δ i ≫ δ j.succ = δ j ≫ δ i.castSucc :=
  by
  ext k
  dsimp [δ, Fin.succAbove]
  rcases i with ⟨i, _⟩
  rcases j with ⟨j, _⟩
  rcases k with ⟨k, _⟩
  split_ifs <;> · simp at * <;> omega

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