getElem?_scanr_zero

Mathlib.Data.List.Scan

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

English

The first element of scanr, as an optional value, is some foldr f b l.

Русский

Первый элемент scanr, как опциональное значение, равен some (foldr f b l).

LaTeX

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

Lean4

theorem getElem?_scanr_zero : (scanr f b l)[0]? = foldr f b l := by simp

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

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

Разделы

Аффилиация

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