Finset filter map

Stream: Is there code for X?

[Marcus Rossel]

Is there some function like:

def finset.filter_map (f : finset X) (g : X -> option Y) : finset Y

... such that f.filter_map g contains all values resulting from mapping f through g which are not none?

[Yaël Dillies]

def finset.filter_map (f : finset X) (g : X -> option Y) : finset Y :=
(f.map g).erase_none