map_ret

Mathlib.Data.WSeq.Basic

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

English

Mapping with the return constructor commutes with return: map f (ret a) = ret (f a).

Русский

Отображение через возврaщение совместимо с возвратом: map f (ret a) = ret (f a).

LaTeX

$$$$ \\operatorname{map} f (\\mathrm{ret}\\ a) = \\mathrm{ret}\\ (f\\ a) $$$$

Lean4

@[simp]
theorem map_ret (f : α → β) (a) : map f (ret a) = ret (f a) := by simp [ret]

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

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

Разделы

Аффилиация

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