ret_bind

Mathlib.Data.WSeq.Relation

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

English

The interaction of bind with ret reduces to map, i.e., bind (ret a) f ~ʷ map f a.

Русский

Взаимодействие bind и ret даёт сокращение к map: bind (ret a) f ~ʷ map f a.

LaTeX

$$$ \forall a, f : \alpha \to \mathrm{WSeq}\,\beta,\; \mathrm{bind}(\mathrm{ret}\, a)\ f ~ʷ \mathrm{map}\ f\ a$$$

Lean4

@[simp]
theorem ret_bind (a : α) (f : α → WSeq β) : bind (ret a) f ~ʷ f a := by simp [bind]

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

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

Разделы

Аффилиация

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