inits_cons

Mathlib.Data.List.Infix

URI: https://scilib.ai/kg/mathlib#List.inits_cons

English

The initial segments of a cons list satisfy inits (a :: l) = [] :: map (a ::) (inits l).

Русский

Начальные отрезки списка, сформированного как a :: l, равны [] :: map (a ::) (inits l).

LaTeX

$$$\text{inits}(a :: l) = [] :: \text{inits}(l) \mapsto (\lambda t. a :: t).$$$

Lean4

theorem inits_cons (a : α) (l : List α) : inits (a :: l) = [] :: l.inits.map fun t => a :: t := by simp

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

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

Разделы

Аффилиация

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