corec

Mathlib.Data.Stream.Defs

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

Lean4

/-- Given functions `f : α → β` and `g : α → α`, `corec f g` creates a stream by:
1. Starting with an initial value `a : α`
2. Applying `g` repeatedly to get a stream of α values
3. Applying `f` to each value to convert them to β
-/
def corec (f : α → β) (g : α → α) : α → Stream' β := fun a => map f (iterate g a)

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

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

Разделы

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

Аффилиация

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