reverse_cons

Mathlib.Data.Vector.Snoc

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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