English
Let f be a partial function α → Option β and g : α → β. Then l.filterMap f = l.map g if and only if f x = Some(g x) for every x in l.
Русский
Пусть f: α → Option β и g: α → β. Тогда l.filterMap f = l.map g тогда и только тогда, когда для каждого x из l выполняется f x = Some(g x).
LaTeX
$$$\forall l:\, List\;\alpha\;\; f:\, \alpha \to Option\;\beta\;\; g:\, \alpha \to \beta,\;\; l.filterMap f = l.map g \iff \ \forall x \in l,\; f x = \text{Some}(g x)$$$
Lean4
theorem filterMap_eq_map_iff_forall_eq_some {f : α → Option β} {g : α → β} {l : List α} :
l.filterMap f = l.map g ↔ ∀ x ∈ l, f x = some (g x)
where
mp :=
by
induction l with
| nil => simp
| cons a l ih => ?_
rcases ha : f a with - | b
· intro h
have : (filterMap f l).length = l.length + 1 := by grind
grind
· simp +contextual [ha, ih]
mpr h := Eq.trans (filterMap_congr <| by simpa) (congr_fun filterMap_eq_map _)
