filter_map — Mathlib

English

Filtering after mapping equals mapping after filtering with the preimage predicate p∘f.

Русский

После отображения фильтрация равна отображению после фильтрации по предикату p∘f.

LaTeX

$$$\\mathrm{filter}_p(\\mathrm{map} f s) = \\mathrm{map} f (\\mathrm{filter} (p \\circ f) s)$$$

Lean4

theorem filter_map (f : β → α) (s : Multiset β) : filter p (map f s) = map f (filter (p ∘ f) s) :=
  Quot.inductionOn s fun l => by simp [List.filter_map];
    rfl
      -- TODO: rename to `map_filter` when the deprecated alias above is removed.

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