map_eq

Mathlib.Data.Stream.Init

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

Lean4

theorem map_eq (s : Stream' α) : map f s = f (head s) :: map f (tail s) := by
  rw [← Stream'.eta (map f s), tail_map, head_map]

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

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

Разделы

Аффилиация

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