head_scanr

Mathlib.Data.List.Scan

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

← MathLib Explorer

English

If scanr f b l is nonempty, its head equals foldr f b l.

Русский

Если scanr f b l непуст, её голова равна foldr f b l.

LaTeX

$$$$\forall l:\mathrm{List}(\alpha),\, (\operatorname{Ne}(\operatorname{scanr} f b l, \varnothing)) \Rightarrow (\operatorname{scanr} f b l).head(h) = \operatorname{foldr} f b l.$$$$

Lean4

@[simp]
theorem head_scanr (h : scanr f b l ≠ []) : (scanr f b l).head h = foldr f b l := by cases l <;> simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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