bind — Mathlib

English

The bind operation for filters is defined in the standard monadic way via map and join.

Русский

Операция bind для фильтров определяется в стандартном монадином виде через map и join.

LaTeX

$$$\text{bind}(f,m) = \mathrm{join}(\mathrm{map}(m,f)).$$$

Lean4

/-- The monadic bind operation on filter is defined the usual way in terms of `map` and `join`.

Unfortunately, this `bind` does not result in the expected applicative. See `Filter.seq` for the
applicative instance. -/
def bind (f : Filter α) (m : α → Filter β) : Filter β :=
  join (map m f)

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