getElem_scanl_zero

Mathlib.Data.List.Scan

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

English

The first element of scanl equals b, i.e., (scanl f b l)[0] = b.

Русский

Первый элемент scanl равен b: (scanl f b l)[0] = b.

LaTeX

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

Lean4

@[simp]
theorem getElem_scanl_zero : (scanl f b l)[0] = b := by cases l <;> simp

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

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

Разделы

Аффилиация

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