pmap_res — Mathlib

English

The pmap of the res-function along l is equal to map f of the intersection of l with the principal filter on s.

Русский

Образ pmap для частичной функции res равен образованию через f пересечения фильтра l с принципиальным фильтром на s.

LaTeX

$$$ \\mathrm{pmap}(\\mathrm{PFun.res}\\ f\\ s)\\ l = \\mathrm{map}\\ f\\ (l \\wedge 𝓟 s) $$$

Lean4

theorem pmap_res (l : Filter α) (s : Set α) (f : α → β) : pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s) :=
  by
  ext t
  simp only [PFun.core_res, mem_pmap, mem_map, mem_inf_principal, imp_iff_not_or]
  rfl

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