δ_comp_δ_nat — Mathlib

English

For natural indices i, j with i ≤ j, the δ maps satisfy δ_i ∘ δ_{j+1} = δ_j ∘ δ_i.

Русский

Для натуральных индексов i, j с i ≤ j выполняется δ_i ∘ δ_{j+1} = δ_j ∘ δ_i.

LaTeX

$$$\delta_{i} \circ \delta_{j+1} = \delta_{j} \circ \delta_{i} \quad\text{при } i \le j$$$

Lean4

/-- A version of δ_comp_δ with indices in ℕ satisfying relevant inequalities. -/
theorem δ_comp_δ_nat {n} (i j : ℕ) (hi : i < n + 2) (hj : j < n + 2) (H : i ≤ j) :
    δ ⟨i, hi⟩ ≫ δ ⟨j + 1, by cutsat⟩ = δ ⟨j, hj⟩ ≫ δ ⟨i, by cutsat⟩ :=
  δ_comp_δ (n := n) (i := ⟨i, by cutsat⟩) (j := ⟨j, by cutsat⟩) (by simpa)

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