length_scanl

Mathlib.Data.List.Scan

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

English

The length of the scanl sequence obtained from l is |l| + 1.

Русский

Длина последовательности scanl, получаемой из l, равна |l| + 1.

LaTeX

$$$$\operatorname{length}(\operatorname{scanl} f b l) = \operatorname{length}(l) + 1.$$$$

Lean4

@[simp]
theorem length_scanl (b : β) (l : List α) : length (scanl f b l) = l.length + 1 := by
  induction l generalizing b <;> simp_all

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

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

Разделы

Аффилиация

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