cons_zero

Mathlib.Data.Fin.Tuple.Basic

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

English

Let x be the first element and p the tail of a tuple; then the concatenated tuple has x at the first position: (cons x p)(0) = x.

Русский

Пусть x — первый элемент кортежа, а p — хвост; тогда конc x p имеет x на первой позиции: (cons x p)(0) = x.

LaTeX

$$$(\\\\mathrm{cons}(x,p))(0) = x$$$

Lean4

@[simp]
theorem cons_zero : cons x p 0 = x := by simp [cons]

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

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

Разделы

Аффилиация

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