filter_filterMap — Mathlib

English

Applying filter to a mapped multiset distributes over filterMap with guard on p.

Русский

Применение фильтра к отображённому мультиету распределяется по filterMap с условием p.

LaTeX

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

Lean4

theorem filter_filterMap (f : α → Option β) (p : β → Prop) [DecidablePred p] (s : Multiset α) :
    filter p (filterMap f s) = filterMap (fun x => (f x).filter p) s :=
  Quot.inductionOn s fun _ => congr_arg ofList List.filter_filterMap

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