lift — Mathlib

English

A variant of bind using a function g: Set α → Filter β, defined by lift(f,g) = ⨅ s ∈ f, g s.

Русский

Вариант связывания, где используется функция g: Set α → Filter β, определяется как lift(f,g) = ⨅ s ∈ f, g s.

LaTeX

$$$\mathrm{lift}(f,g) = \bigwedge_{s \in f} g(s).$$$

Lean4

/-- A variant on `bind` using a function `g` taking a set instead of a member of `α`.
This is essentially a push-forward along a function mapping each set to a filter. -/
protected def lift (f : Filter α) (g : Set α → Filter β) :=
  ⨅ s ∈ f, g s

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