insertNth_apply_cycleRange_symm — Mathlib

English

For any α, p: Fin(n+1) → α, a: α, x: Fin n → α, and j: Fin(n+1), we have (p.insertNth a x)(p.cycleRange.symm j) = (Fin.cons a x)(j).

Русский

Для любого α, p: Fin(n+1)→α, a: α, x: Fin n→α и j: Fin(n+1) выполняется (p.insertNth a x)(p.cycleRange.symm j) = (Fin.cons a x)(j).

LaTeX

$$$(p.insertNth\ a\ x)(p.cycleRange^{-1}(j)) = (\mathrm{Fin}.cons\ a\ x)(j)$$$

Lean4

@[simp]
theorem insertNth_apply_cycleRange_symm {α : Type*} (p : Fin (n + 1)) (a : α) (x : Fin n → α) (j : Fin (n + 1)) :
    (p.insertNth a x : _ → α) (p.cycleRange.symm j) = (Fin.cons a x : _ → α) j := by cases j using Fin.cases <;> simp

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