English
filterMap f s f_inj is the Finset of β consisting of all values b such that f a = some b for some a ∈ s; it is defined by taking the underlying multiset and removing duplicates according to f_inj.
Русский
filterMap f s f_inj образует конечное множество β consisting of all values b such that f(a) = some b for some a ∈ s; он задаётся через базовую мультисетную операцию filterMap с учётом вложенной инъекции.
LaTeX
$$$\\text{filterMap } f\\ s\\ f_{inj} = \\langle s.1.filterMap f,\\ s.2.filterMap f f_{inj} \\rangle$$$
Lean4
/-- `filterMap f s` is a combination filter/map operation on `s`.
The function `f : α → Option β` is applied to each element of `s`;
if `f a` is `some b` then `b` is included in the result, otherwise
`a` is excluded from the resulting finset.
In notation, `filterMap f s` is the finset `{b : β | ∃ a ∈ s, f a = some b}`. -/
-- TODO: should there be `filterImage` too?
def filterMap (f : α → Option β) (s : Finset α) (f_inj : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') : Finset β :=
⟨s.val.filterMap f, s.nodup.filterMap f f_inj⟩
