const

Mathlib.Data.Stream.Defs

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

Lean4

/-- The constant stream: `Stream'.get n (Stream'.const a) = a`. -/
def const (a : α) : Stream' α := fun _ => a

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

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

Разделы

Аффилиация

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