erase_getElem — Mathlib

English

For a nodup list l, and i a valid index, l.erase(l[i]) equals l.eraseIdx(i).

Русский

Для безповторного списка l и допустимого индекса i, l.erase(l[i]) = l.eraseIdx i.

LaTeX

$$$[DecidableEq \\alpha] \\{l : List \\alpha\\} (hl : l.Nodup) (i : Fin(l.length)) : l.erase(l[i]) = l.eraseIdx i.val$$$

Lean4

theorem erase_getElem [DecidableEq α] {l : List α} (hl : l.Nodup) (i : Nat) (h : i < l.length) :
    l.erase l[i] = l.eraseIdx ↑i := by
  induction l generalizing i with
  | nil => simp
  | cons a l IH =>
    cases i with
    | zero => simp
    | succ i => grind

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