pmap — Mathlib

English

The forward map of a filter under a partial function: pmap f l is defined as rmap f.graph' l, i.e., pushing forward along the graph of f.

Русский

Переход фильтра через частичную функцию задается как передача через граф функции: pmap f l = rmap f.graph' l.

LaTeX

$$$ \\mathrm{pmap}\\, f\\, l = \\mathrm{rmap}\\, f.\\mathrm{graph}'\\, l $$$

Lean4

/-- The forward map of a filter under a partial function. Generalization of `Filter.map` to partial
functions. -/
def pmap (f : α →. β) (l : Filter α) : Filter β :=
  Filter.rmap f.graph' l

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