length_inits

Mathlib.Data.List.Infix

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

English

The length of the inits of a list l is length(l) + 1.

Русский

Длина инитов списка l равна длине l плюс 1.

LaTeX

$$$\\operatorname{length}(\\operatorname{inits}(l)) = \\operatorname{length}(l) + 1$$$

Lean4

@[simp]
theorem length_inits (l : List α) : length (inits l) = length l + 1 := by simp [inits_eq_tails]

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

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

Разделы

Аффилиация

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