take_succ_cons

Mathlib.Data.Seq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.take_succ_cons

English

Taking n+1 elements from cons x s yields x prepended to take n elements of s.

Русский

При взятии n+1 элементов из cons x s получаем x в начале и take n элементов из s.

LaTeX

$$$\mathrm{take}(n+1, \mathrm{cons}(x, s)) = x :: \mathrm{take}(n, s)$$$

Lean4

@[simp]
theorem take_succ_cons {n : ℕ} {x : α} {s : Seq α} : (cons x s).take (n + 1) = x :: s.take n := by rfl

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

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

Разделы

Аффилиация

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