lift' — Mathlib

English

Specialize lift to h: Set α → Set β by setting f.lift' (h) = f.lift (𝓟 ∘ h).

Русский

Специализируем lift на h: Set α → Set β, задавая f.lift' (h) = f.lift (𝓟 ∘ h).

LaTeX

$$$\mathrm{lift}'(f,h) = f\,\mathrm{lift}( \mathcal{P} \circ h ).$$$

Lean4

/-- Specialize `lift` to functions `Set α → Set β`. This can be viewed as a generalization of `map`.
This is essentially a push-forward along a function mapping each set to a set. -/
protected def lift' (f : Filter α) (h : Set α → Set β) :=
  f.lift (𝓟 ∘ h)

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