pcomap' — Mathlib

English

The inverse map of a filter under a partial function, defined as rcomap' along the graph of the function.

Русский

Обратное отображение фильтра через частичную функцию задается через rcomap' графа функции.

LaTeX

$$$ \\mathrm{pcomap}'\\, f\\, l = \\mathrm{rcomap}'\\, f.\\mathrm{graph}'\\, l $$$

Lean4

/-- Inverse map of a filter under a partial function. One generalization of `Filter.comap` to
partial functions. -/
def pcomap' (f : α →. β) (l : Filter β) : Filter α :=
  Filter.rcomap' f.graph' l

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