erase_getElem — Mathlib

English

For any i with i < length l, erasing the i-th element of l yields a list that is a permutation of erasing by index i.

Русский

При любом i с i < длина(l) удаление i-го элемента списка приводит к списку, являющемуся перестановкой от удаления элемента по индексу i.

LaTeX

$$$ \\Perm (l.erase (l[i])) (l.eraseIdx i) $$$

Lean4

theorem erase_getElem [DecidableEq ι] {l : List ι} {i : ℕ} (hi : i < l.length) : Perm (l.erase l[i]) (l.eraseIdx i) :=
  by
  induction l generalizing i with
  | nil => simp
  | cons a l IH => cases i with grind

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