getElem_scanr_zero

Mathlib.Data.List.Scan

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

English

The first element of scanr equals the foldr of the list: (scanr f b l)[0] = foldr f b l.

Русский

Первый элемент scanr равен свёртке списка: (scanr f b l)[0] = foldr f b l.

LaTeX

$$$$ (\operatorname{scanr} f b l)[0] = \operatorname{foldr} f b l. $$$$

Lean4

@[simp]
theorem getElem_scanr_zero : (scanr f b l)[0] = foldr f b l := by cases l <;> simp

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

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

Разделы

Аффилиация

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