insertIdx_eraseIdx_getElem

Mathlib.Data.List.InsertIdx

URI: https://scilib.ai/kg/mathlib#List.insertIdx_eraseIdx_getElem

English

If n < length l, then (l.eraseIdx n).insertIdx n l[n] equals l.

Русский

Если n меньше длины l, то (l.eraseIdx n).insertIdx n l[n] = l.

LaTeX

$$$(l.eraseIdx n).insertIdx n \\ l[n] = l \\quad (n < \\operatorname{length} l)$$$

Lean4

theorem insertIdx_eraseIdx_getElem {l : List α} {n : ℕ} (hn : n < length l) : (l.eraseIdx n).insertIdx n l[n] = l := by
  simp [hn.ne]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru