zip_inits_tails

Mathlib.Data.Stream.Init

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

Lean4

theorem zip_inits_tails (s : Stream' α) : zip appendStream' (inits s) (tails s) = const s :=
  by
  apply Stream'.ext; intro n
  rw [get_zip, get_inits, get_tails, get_const, take_succ, cons_append_stream, append_take_drop, Stream'.eta]

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

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

Разделы

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

Аффилиация

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