snoc_cons

Mathlib.Data.Vector.Snoc

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

English

snoc xs x equals xs appended with the singleton [x], i.e., (xs.snoc x) = xs ++ x ::ᵥ Vector.nil.

Русский

snoc xs x равен xs, дополненному единичным списком [x], то есть (xs.snoc x) = xs ++ x ::ᵥ Vector.nil.

LaTeX

$$$ (xs.snoc x) = xs ++ x ::ᵥ Vector.nil $$$

Lean4

@[simp]
theorem snoc_cons : (x ::ᵥ xs).snoc y = x ::ᵥ (xs.snoc y) :=
  rfl

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

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

Разделы

Аффилиация

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