set_perm_cons_eraseIdx — Mathlib

English

If n < length(l), then l.set n a is permuted with a :: l.eraseIdx n.

Русский

Если n < длины l, то l.set n a переставляется в a :: l.eraseIdx n.

LaTeX

$$$\\forall n:\\, n < |l| \\Rightarrow \\forall a:\\, \\ l.set(n,a) \\sim (a :: l.eraseIdx(n)).$$$

Lean4

theorem set_perm_cons_eraseIdx {n : ℕ} (h : n < l.length) (a : α) : l.set n a ~ a :: l.eraseIdx n :=
  by
  rw [← insertIdx_eraseIdx_self h.ne]
  apply perm_insertIdx
  rw [length_eraseIdx_of_lt h]
  exact Nat.le_sub_one_of_lt h

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