filterMap_filter — Mathlib

English

Filtering a multiset with p and then applying filterMap is the same as applying filterMap to each element, keeping only those with p.

Русский

Фильтрация мультисе-та по p, затем filterMap, эквивалентна filterMap, где каждый элемент обрабатывается так, чтобы удовлетворял p.

LaTeX

$$$\operatorname{filterMap} f (\operatorname{filter} p s) = \operatorname{filterMap} (\lambda x. (f x).filter p) s$$$

Lean4

theorem filterMap_filter (f : α → Option β) (s : Multiset α) :
    filterMap f (filter p s) = filterMap (fun x => if p x then f x else none) s :=
  Quot.inductionOn s fun l => congr_arg ofList <| by simpa using List.filterMap_filter (f := f) (p := p)

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