snoc_nil

Mathlib.Data.Vector.Snoc

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

English

nil.snoc x = x ::ᵥ nil, i.e., a one-element vector obtained by snoc-ing x to the empty vector.

Русский

nil.snoc x = x ::ᵥ nil, то есть вектор с одним элементом, полученный применением snoc к пустому вектору.

LaTeX

$$$\text{nil}.snoc x = x ::ᵥ \text{nil}$$$

Lean4

@[simp]
theorem snoc_nil : (nil.snoc x) = x ::ᵥ nil :=
  rfl

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

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

Разделы

Аффилиация

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