cons_apply_cycleRange — Mathlib

English

The action of Fin.cons a x on p.cycleRange j equals p.insertNth a x j.

Русский

Действие Fin.cons a x на p.cycleRange j даёт p.insertNth a x j.

LaTeX

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

Lean4

@[simp]
theorem cons_apply_cycleRange {α : Type*} (a : α) (x : Fin n → α) (p j : Fin (n + 1)) :
    (Fin.cons a x : _ → α) (p.cycleRange j) = (p.insertNth a x : _ → α) j := by
  rw [← insertNth_apply_cycleRange_symm, Equiv.symm_apply_apply]

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