map_think' — Mathlib

English

For every function f: α → β and computation s of type α, applying map to think s equals think applied to map f s: f <$> think s = think (f <$> s).

Русский

Для каждой функции f: α → β и вычисления s типа α выполняется f ∘ think s = think ∘ f ∘ s, то есть f <$> think s = think (f <$> s).

LaTeX

$$$\operatorname{map} f\big(\operatorname{think} s\big) = \operatorname{think}\big(\operatorname{map} f\, s\big)$$$

Lean4

@[simp]
theorem map_think' {α β} : ∀ (f : α → β) (s), f <$> think s = think (f <$> s) :=
  map_think

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