unfolds_head_eq

Mathlib.Data.Stream.Init

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

Lean4

theorem unfolds_head_eq : ∀ s : Stream' α, unfolds head tail s = s := fun s =>
  Stream'.ext fun n => get_unfolds_head_tail n s

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

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

Разделы

Аффилиация

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