get_append_cons_zero

Mathlib.Data.Vector.Basic

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

English

Given a vector obtained by prepending x to xs and then concatenating with ys, the first element (index 0) is x.

Русский

Для вектора, полученного добавлением x в начало xs и конкатенацией с ys, первый элемент равен x.

LaTeX

$$$\\mathrm{get}(\\,x \\;::\\!\\!\\!{xs} \\;++\\; ys\\,)\\n0 = x$$$

Lean4

@[simp]
theorem get_append_cons_zero : get (x ::ᵥ xs ++ ys) 0 = x :=
  rfl

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

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

Разделы

Аффилиация

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