English
Let f be injective. Then (l.filter p).map f equals (l.map f).filter b => ∃ a, p a ∧ f a = b, under suitable decidability. This expresses that mapping after filtering mirrors filtering after mapping under injectivity.
Русский
Пусть f инъективна. Тогда (l.filter p).map f равно (l.map f).filter b => ∃ a, p a ∧ f a = b, при допустимости:DecidablePred.
LaTeX
$$$$ (\\operatorname{filter} p\, l).map f = (\\operatorname{map} f\, l).\\operatorname{filter} (\\lambda b. \\exists a, p a \\wedge f a = b). $$$$
Lean4
theorem map_filter {f : α → β} (hf : Injective f) (l : List α) [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
(l.filter p).map f = (l.map f).filter fun b => ∃ a, p a ∧ f a = b := by simp [comp_def, filter_map, hf.eq_iff]
