scanr_cons

Mathlib.Data.List.Scan

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

Lean4

@[simp]
theorem scanr_cons : scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l :=
  by
  simp only [scanr, foldr, cons.injEq, and_true]
  induction l generalizing a with
  | nil => rfl
  | cons hd tl ih => simp only [foldr, ih]

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

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

Разделы

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

Аффилиация

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