vecAppend_empty

Mathlib.Data.Fin.VecNotation

URI: https://scilib.ai/kg/mathlib#Matrix.vecAppend_empty

English

Concatenating with an empty vector on the right yields the left vector.

Русский

Сцепление с пустым вектором справа даёт левый вектор.

LaTeX

$$$\\operatorname{vecAppend}(rfl,u,\\![]) = u$$$

Lean4

@[simp]
theorem vecAppend_empty (v : Fin n → α) : vecAppend rfl v ![] = v :=
  by
  ext
  simp [vecAppend_eq_ite]

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

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

Разделы

Аффилиация

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