bind_map — Mathlib

English

Let m: α → β, F a filter on α, and G: β → Filter γ. Then (bind (map m F) G) equals (bind F (G ∘ m)).

Русский

Пусть m: α → β, F — фильтр на α, и G : β → фильтр γ. Тогда (bind (map m F) G) равно (bind F (G ∘ m)).

LaTeX

$$$ \mathrm{bind}(\mathrm{map}(m,f), g) = \mathrm{bind}(f, g \circ m) $$$

Lean4

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

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