cons_succ

Mathlib.Data.Fin.Tuple.Basic

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

English

The value of cons at i.succ equals p i: cons x p (i.succ) = p i.

Русский

Значение cons в i.succ равно p i: cons x p (i.succ) = p i.

LaTeX

$$$\forall i \in \mathrm{Fin}(n),\ \mathrm{cons}(x,p)(i.succ) = p(i)$$$

Lean4

@[simp]
theorem cons_succ : cons x p i.succ = p i := by simp [cons]

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

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

Разделы

Аффилиация

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