filterMap_filterMap — Mathlib

English

Sequential filterMaps compose: filtering with f and then g equals filtering with the composition via bind.

Русский

Последовательная фильтрация через f и затем через g эквивалентна фильтрации через связывание (bind) на составном выражении.

LaTeX

$$$\operatorname{filterMap} g (\operatorname{filterMap} f s) = \operatorname{filterMap} (\lambda x. (f x).bind g) s$$$

Lean4

theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (s : Multiset α) :
    filterMap g (filterMap f s) = filterMap (fun x => (f x).bind g) s :=
  Quot.inductionOn s fun _ => congr_arg ofList List.filterMap_filterMap

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