eraseIdx_insertIdx_self — Mathlib

English

Erasing an element after inserting at the same index returns the original vector: eraseIdx i (insertIdx a i v) = v.

Русский

Удаление элемента после вставки на тот же индекс возвращает исходный вектор: eraseIdx i (insertIdx a i v) = v.

LaTeX

$$$ eraseIdx\\ i\\ (insertIdx\\ a\\ i\\ v) = v $$$

Lean4

theorem eraseIdx_insertIdx_self {v : Vector α n} {i : Fin (n + 1)} : eraseIdx i (insertIdx a i v) = v :=
  Subtype.eq (List.eraseIdx_insertIdx_self ..)

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