map_bind — Mathlib

English

Mapping after binding equals binding after mapping: map m (bind f g) = bind f (map m ∘ g).

Русский

Отображение после связывания равно связыванию после отображения: map m (bind f g) = bind f (map m ∘ g).

LaTeX

$$map_bind {α β} (m : β → γ) (f : Filter α) (g : α → Filter β) : map m (bind f g) = bind f (map m ∘ g)$$

Lean4

theorem map_bind {α β} (m : β → γ) (f : Filter α) (g : α → Filter β) : map m (bind f g) = bind f (map m ∘ g) :=
  rfl

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