map_filterMap — Mathlib

English

Applying map after filterMap is the same as applying filterMap with the mapped option values.

Русский

Применение map после filterMap эквивалентно применению filterMap с отображением.

LaTeX

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

Lean4

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

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