snoc_eq_append

Mathlib.Data.Fin.Tuple.Basic

URI: https://scilib.ai/kg/mathlib#Fin.snoc_eq_append

← MathLib Explorer

English

Snoc xs x equals append xs (cons x Fin.elim0).

Русский

Snoc xs x равно append xs (cons x Fin.elim0).

LaTeX

$$$\\\\operatorname{snoc} xs x = \\\\operatorname{append} xs (\\\\operatorname{cons} x \\\\mathrm{elim0})$$$

Lean4

/-- `Fin.snoc` is the same as appending a one-tuple -/
theorem snoc_eq_append {α : Sort*} (xs : Fin n → α) (x : α) : snoc xs x = append xs (cons x Fin.elim0) :=
  (append_right_eq_snoc xs (cons x Fin.elim0)).symm

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

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

Разделы

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

Аффилиация

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