insertIdx_eraseIdx_self — Mathlib

English

If n is a valid index, then erasing the nth element and inserting a at n yields setting the nth element to a.

Русский

Если n допустим, удаление n-го элемента и вставка a на позицию n эквивалентны замене n-го элемента на a.

LaTeX

$$$(l.eraseIdx n).insertIdx n a = l.set n a$$$

Lean4

/-- Erasing `n`th element of a list, then inserting `a` at the same place
is the same as setting `n`th element to `a`.

We assume that `n ≠ length l`, because otherwise LHS equals `l ++ [a]` while RHS equals `l`. -/
@[simp]
theorem insertIdx_eraseIdx_self {l : List α} {n : ℕ} (hn : n ≠ length l) (a : α) :
    (l.eraseIdx n).insertIdx n a = l.set n a := by induction n generalizing l <;> cases l <;> simp_all

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