length_scanr

Mathlib.Data.List.Scan

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

English

The length of scanr f b l is length(l) + 1.

Русский

Длина scanr f b l равна длине l плюс 1.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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