filterMap_map — Mathlib

English

Applying filterMap after mapping by a function is the same as filtering by the composed operation.

Русский

Применение filterMap после map эквивалентно фильтрации через композицию операций.

LaTeX

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

Lean4

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

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