get_inits

Mathlib.Data.List.Infix

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

English

For l and Fin(length(inits(l))), inits(l).get n = l.take n.

Русский

Для l и Fin(length(inits(l))) выполняется inits(l).get n = l.take n.

LaTeX

$$$(\\operatorname{inits}(l)).get n = l.take n$$$

Lean4

theorem get_inits (l : List α) (n : Fin (length (inits l))) : (inits l).get n = l.take n := by simp

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

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

Разделы

Аффилиация

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