getElem?_scanl_zero

Mathlib.Data.List.Scan

URI: https://scilib.ai/kg/mathlib#List.getElem?_scanl_zero

English

The first element of the scanl sequence is the initial value b, i.e., (scanl f b l)[0]? = some b.

Русский

Первый элемент последовательности scanl равен начальному значению b: (scanl f b l)[0]? = some b.

LaTeX

$$$$ (\mathrm{scanl} \\ f \\ b \\ l)[0]? = \mathrm{some}\ b. $$$$

Lean4

theorem getElem?_scanl_zero : (scanl f b l)[0]? = some b := by cases l <;> simp

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

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

Разделы

Аффилиация

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