English
If a function f from α to Option β has the property that f(a) values uniquely determine a (i.e., f is injective on occurrences), then Nodup is preserved under filterMap along l.
Русский
Если функция f: α → Option β имеет свойство, что выводы f(a) уникальны по значению a (условно инъективность на встречающихся элементах), то применение filterMap к над списку l сохраняет отсутствие повторов.
LaTeX
$$$ (\\forall a,a',b,\\ b \\in f(a) \\Rightarrow b \\in f(a') \\Rightarrow a=a') \\land \\operatorname{Nodup}(l) \\Rightarrow \\operatorname{Nodup}(\\operatorname{filterMap} f\\ l). $$$
Lean4
protected theorem filterMap {f : α → Option β} (h : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
Nodup l → Nodup (filterMap f l) :=
(Pairwise.filterMap f) @fun a a' n b bm b' bm' e => n <| h a a' b' (by rw [← e]; exact bm) bm'
