map_pure'

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.map_pure'

English

For any function f: α → β and any a, map f (pure a) = pure (f a).

Русский

Для любой функции f: α → β и любого a: α выполняется map f (pure a) = pure (f a).

LaTeX

$$$\operatorname{map} f\big(\operatorname{pure} a\big) = \operatorname{pure}\big(f a\big)$$$

Lean4

@[simp]
theorem map_pure' {α β} : ∀ (f : α → β) (a), f <$> pure a = pure (f a) :=
  map_pure

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

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

Разделы

Аффилиация

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