insertIdx_val

Mathlib.Data.Vector.Basic

URI: https://scilib.ai/kg/mathlib#List.Vector.insertIdx_val

English

The underlying list of v.insertIdx a i equals the list v.val with a inserted at position i.1.

Русский

Пусть подложный список v.insertIdx a i равен списку v.val, в котором элемент a вставлен на позиции i.1.

LaTeX

$$$ (v.insertIdx\\ a\\ i).val = v.val.insertIdx i.1\\ a $$$

Lean4

theorem insertIdx_val {i : Fin (n + 1)} {v : Vector α n} : (v.insertIdx a i).val = v.val.insertIdx i.1 a :=
  rfl

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

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

Разделы

Аффилиация

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