cons_val

Mathlib.Data.Vector.Basic

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

English

Adding an element to a vector preserves its value representation: (a ::ᵥ v).val = a :: v.val.

Русский

Добавление элемента к вектору сохраняет его представление в виде списка: (a ::ᵥ v).val = a :: v.val.

LaTeX

$$$(a ::ᵥ v).\\mathrm{val} = a :: v.\\mathrm{val}$$$

Lean4

@[simp]
theorem cons_val (a : α) : ∀ v : Vector α n, (a ::ᵥ v).val = a :: v.val
  | ⟨_, _⟩ => rfl

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

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

Разделы

Аффилиация

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