cons_get_inits_core

Mathlib.Data.Stream.Init

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

Lean4

theorem cons_get_inits_core (a : α) (n : ℕ) (l : List α) (s : Stream' α) :
    (a :: get (initsCore l s) n) = get (initsCore (a :: l) s) n := by
  induction n generalizing l s with
  | zero => rfl
  | succ n ih =>
    rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]
    rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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