scanl_cons

Mathlib.Data.List.Scan

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

English

Scanl on a cons lists satisfies a simple formula: scanl f b (a :: l) = [b] ++ scanl f (f b a) l.

Русский

Scanl на конc-список удовлетворяет формуле: scanl f b (a :: l) = [b] ++ scanl f (f b a) l.

LaTeX

$$$$\operatorname{scanl} f b (a\;::\;l) = [b] \;++\; \operatorname{scanl} f (f\;b\;a) l.$$$$

Lean4

@[simp]
theorem scanl_cons : scanl f b (a :: l) = [b] ++ scanl f (f b a) l := by simp only [scanl, singleton_append]

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

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

Разделы

Аффилиация

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