erase_get — Mathlib

English

[DecidableEq α] {l : List α} (hl : l.Nodup) (i : Nat) (h : i < l.length) : l.erase l[i] = l.eraseIdx ↑i

Русский

[DecidableEq α] {l : List α} (hl : l.Nodup) (i : Nat) (h : i < l.length) : l.erase l[i] = l.eraseIdx i

LaTeX

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

Lean4

theorem erase_get [DecidableEq α] {l : List α} (hl : l.Nodup) (i : Fin l.length) : l.erase (l.get i) = l.eraseIdx ↑i :=
  by simp [erase_getElem, hl]

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