English
If f is injective, then mapping after filtering equals filtering after mapping with a predicate expressed via existence.
Русский
Если отображение инъективно, то отображение после фильтрации эквивалентно фильтрации после отображения с предикатом, задаваемым существованием.
LaTeX
$$$\\mathrm{map}_f (\\mathrm{filter}_p s) = \\mathrm{filter} (\\lambda b. \\exists a, p(a) \\land f(a) = b) (\\mathrm{map} f s)$ при предположении, что f инъективно$$
Lean4
theorem map_filter' {f : α → β} (hf : Injective f) (s : Multiset α) [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
(s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b := by simp [filter_map, hf.eq_iff]
