σ_comp_σ_nat — Mathlib

English

For natural indices i, j with i ≤ j, the degeneracy maps commute as σ_i.castSucc ∘ σ_j = σ_j.succ ∘ σ_i.

Русский

Для натуральных индексов i, j с i ≤ j выполняется σ_i.castSucc ∘ σ_j = σ_j.succ ∘ σ_i.

LaTeX

$$$\sigma_{i}^{\mathrm{castSucc}} \circ \sigma_j = \sigma_{j+1} \circ \sigma_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 + 1) (hj : j < n + 1) (H : i ≤ j) :
    σ ⟨i, by cutsat⟩ ≫ σ ⟨j, hj⟩ = σ ⟨j + 1, by cutsat⟩ ≫ σ ⟨i, hi⟩ :=
  σ_comp_σ (n := n) (i := ⟨i, by cutsat⟩) (j := ⟨j, by cutsat⟩) (by simpa)

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