reverse_snoc

Mathlib.Data.Vector.Snoc

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

← MathLib Explorer

English

reverse (xs.snoc x) = x ::ᵥ reverse xs.

Русский

reverse (xs.snoc x) = x ::ᵥ reverse xs.

LaTeX

$$$\operatorname{reverse}(xs.snoc x) = x ::ᵥ \operatorname{reverse} xs$$$

Lean4

@[simp]
theorem reverse_snoc : reverse (xs.snoc x) = x ::ᵥ (reverse xs) :=
  by
  cases xs
  simp only [reverse, snoc, cons, toList_mk]
  congr
  simp [toList, append_def]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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